:: The Sum and Product of Finite Sequences of Complex Numbers
::  by Keiichi Miyajima and Takahiro Kato
::
:: Received January 12, 2010
:: Copyright (c) 2010 Association of Mizar Users

environ

 vocabularies FINSEQ_1, FINSEQ_2, ARYTM_1, FUNCT_1, RELAT_1, BINOP_1, SETWISEO,
      SQUARE_1, FUNCOP_1, RVSUM_1, RVSUM_2, CARD_3, XBOOLE_0, COMPLEX1,
      XCMPLX_0, VALUED_0, BINOP_2, ZFMISC_1, NUMBERS, SUBSET_1, NAT_1, TARSKI,
      ORDINAL4, ORDINAL1, ARYTM_3, CARD_1, VALUED_1, XREAL_0;
 notations TARSKI, SUBSET_1, ZFMISC_1, ORDINAL1, NUMBERS, VALUED_0, XBOOLE_0,
      XCMPLX_0, XREAL_0, COMPLEX1, NAT_1, SQUARE_1, RELAT_1, FUNCT_1, PARTFUN1,
      BINOP_2, FUNCT_2, BINOP_1, FUNCOP_1, FINSEQ_1, FINSEQ_2, VALUED_1, SEQ_4,
      FINSEQOP, SETWOP_2, RVSUM_1;
 constructors BINOP_1, COMPLEX1, SETWISEO, SQUARE_1, BINOP_2, FINSEQOP,
      FINSOP_1, RELSET_1, RVSUM_1, SEQ_4;
 registrations FUNCT_1, FUNCT_2, FUNCOP_1, NUMBERS, XREAL_0, BINOP_2, MEMBERED,
      FINSEQ_1, FINSEQ_2, VALUED_0, VALUED_1, RELAT_1, RVSUM_1, NEWTON;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions BINOP_1, FINSEQOP, FINSEQ_1, SQUARE_1, FINSEQ_2, TARSKI, VALUED_1,
      XCMPLX_0, RVSUM_1, COMPLEX1, XBOOLE_0, SEQ_4;
 theorems FUNCT_1, FUNCT_2, FINSEQ_1, FUNCOP_1, FINSEQ_2, FINSEQOP, SETWOP_2,
      RELAT_1, FINSOP_1, ZFMISC_1, XCMPLX_0, BINOP_2, FINSEQ_3, VALUED_0,
      VALUED_1, RFUNCT_1, RVSUM_1, SEQ_4;
 schemes NAT_1, FUNCT_2;

begin :: Auxiliary theorems

definition let F be complex-valued Relation;
  redefine func rng F -> Subset of COMPLEX;
  coherence by VALUED_0:def 1;
end;

registration
  let D be non empty set;
  let F be Function of COMPLEX,D;
  let F1 be complex-valued FinSequence;
  cluster F*F1 -> FinSequence-like;
  coherence
  proof
    consider n1 being Nat such that
A1: dom F1 = Seg n1 by FINSEQ_1:def 2;
    take n1;
    dom F = COMPLEX & rng F1 c= COMPLEX by FUNCT_2:def 1;
    hence thesis by A1,RELAT_1:46;
  end;
end;

reserve s for set,
  i,j for Nat,
  x,x1,x2 for Element of COMPLEX,
  c,c1,c2,c3 for complex number,
  F,F1,F2 for complex-valued FinSequence,
  R,R1,R2 for i-long FinSequence of COMPLEX;

definition
  func sqrcomplex -> UnOp of COMPLEX means :Def1:
  for c holds it.c = c^2;
  existence
  proof
    deffunc F(Element of COMPLEX) = $1^2;
    consider G being Function of COMPLEX,COMPLEX such that
A1: for x being Element of COMPLEX holds G.x = F(x) from FUNCT_2:sch 4;
    take G;
    let c;
    c in COMPLEX by XCMPLX_0:def 2;
    hence thesis by A1;
  end;
  uniqueness
  proof
    let G1,G2 be UnOp of COMPLEX such that
A2: for c holds G1.c = c^2 and
A3: for c holds G2.c = c^2;
    now let x;
      G1.(x) = (x)^2 by A2;
      hence G1.x = G2.x by A3;
    end;
    hence thesis by FUNCT_2:113;
  end;
end;

theorem
  sqrcomplex is_distributive_wrt multcomplex
proof
  let x1,x2;
  thus sqrcomplex.(multcomplex.(x1,x2)) = sqrcomplex.(x1*x2) by BINOP_2:def 5
     .= (x1*x2)^2 by Def1
     .= x1^2*x2^2
     .= multcomplex.(x1^2,x2^2) by BINOP_2:def 5
     .= multcomplex.(sqrcomplex.x1,x2^2) by Def1
     .= multcomplex.(sqrcomplex.x1,sqrcomplex.x2) by Def1;
end;

::: generalized COMPLSP1:16

Lm1: (multcomplex[;](c,id COMPLEX)).c1 = c*c1
proof
  reconsider a=c, s=c1 as Element of COMPLEX by XCMPLX_0:def 2;
  thus (multcomplex[;](c,id COMPLEX)).c1 = multcomplex.(a,(id COMPLEX).s)
        by FUNCOP_1:66
    .= multcomplex.(a,s) by FUNCT_1:35
    .= c*c1 by BINOP_2:def 5;
end;

theorem ::: generalized COMPLSP1:17
  c multcomplex is_distributive_wrt addcomplex
proof
  c in COMPLEX by XCMPLX_0:def 2;
  hence thesis by SEQ_4:71,FINSEQOP:55;
end;

begin :: Some Functors on the i-tuples on Complex

Lm2: F is FinSequence of COMPLEX
proof
  thus rng F c= COMPLEX;
end;

definition let F1,F2;
  redefine func F1 + F2 -> FinSequence of COMPLEX equals
  addcomplex.:(F1,F2);
  coherence by Lm2;
  compatibility
  proof
    reconsider F3=F1,F4=F2 as FinSequence of COMPLEX by Lm2;
    let F be FinSequence of COMPLEX;
    dom addcomplex = [:COMPLEX,COMPLEX:] by FUNCT_2:def 1; then
    [:rng F3, rng F4:] c= dom addcomplex by ZFMISC_1:119; then
A1: dom(addcomplex.:(F1,F2)) = dom F1 /\ dom F2 by FUNCOP_1:84;
A2: dom (F1+F2) = dom F1 /\ dom F2 by VALUED_1:def 1;
    thus F = F1+F2 implies F = addcomplex.:(F1,F2)
    proof
      assume A3: F = F1+F2;
      for z being set st z in dom(addcomplex.:(F1,F2)) holds
          F.z = addcomplex.(F1.z,F2.z)
      proof
        let z be set;
        assume z in dom(addcomplex.:(F1,F2));
        hence F.z = F1.z + F2.z by A2,A1,A3,VALUED_1:def 1
                 .= addcomplex.(F1.z,F2.z) by BINOP_2:def 3;
      end;
      hence thesis by A2,A1,A3,FUNCOP_1:27;
    end;
    assume A4: F = addcomplex.:(F1,F2);
    now let c be set;
      assume c in dom F;
      hence F.c = addcomplex.(F1.c,F2.c) by A4,FUNCOP_1:28
               .= F1.c + F2.c by BINOP_2:def 3;
    end;
    hence thesis by A1,A4,VALUED_1:def 1;
  end;
  commutativity
  proof
    let F be FinSequence of COMPLEX;
    let F1,F2;
    assume
A5: F = addcomplex.:(F1,F2);
    reconsider F1,F2 as FinSequence of COMPLEX by Lm2;
A6: dom addcomplex = [:COMPLEX,COMPLEX:] by FUNCT_2:def 1; then
A7: [:rng F2, rng F1:] c= dom addcomplex by ZFMISC_1:119;
    [:rng F1, rng F2:] c= dom addcomplex by A6,ZFMISC_1:119; then
A8: dom(addcomplex.:(F1,F2)) = dom F1 /\ dom F2 by FUNCOP_1:84
   .= dom(addcomplex.:(F2,F1)) by A7,FUNCOP_1:84;
    for z being set st z in dom(addcomplex.:(F2,F1))
      holds F.z = addcomplex.(F2.z,F1.z)
    proof
      let z be set;
      assume z in dom(addcomplex.:(F2,F1));
      hence F.z = addcomplex.(F1.z,F2.z) by A5,A8,FUNCOP_1:28
               .= F1.z + F2.z by BINOP_2:def 3
               .= addcomplex.(F2.z,F1.z) by BINOP_2:def 3;
    end;
    hence thesis by A5,A8,FUNCOP_1:27;
  end;
end;

definition let i,R1,R2;
  redefine func R1 + R2 -> Element of i-tuples_on COMPLEX;
  coherence by FINSEQ_2:140;
end;

theorem
  (R1+R2).s = R1.s + R2.s
proof
  per cases;
  suppose
A1: not s in Seg i; then
A2: not s in dom R2 by FINSEQ_2:144;
A3: not s in dom R1 by A1,FINSEQ_2:144;
    not s in dom(R1+R2) by A1,FINSEQ_2:144;
    hence (R1+R2).s = 0+0 by FUNCT_1:def 4
      .= R1.s + 0 by A3,FUNCT_1:def 4
      .= R1.s + R2.s by A2,FUNCT_1:def 4;
  end;
  suppose s in Seg i; then
    s in dom (R1 + R2) by FINSEQ_2:144;
    hence thesis by VALUED_1:def 1;
  end;
end;

theorem
  <*>COMPLEX + F = <*>COMPLEX
proof
  F is FinSequence of COMPLEX by Lm2;
  hence thesis by FINSEQ_2:87;
end;

theorem
  <*c1*> + <*c2*> = <*c1+c2*>
proof
  reconsider s1=c1, s2=c2 as Element of COMPLEX by XCMPLX_0:def 2;
  <*s1*> + <*s2*> = <*addcomplex.(s1,s2)*> by FINSEQ_2:88
    .= <*c1+c2*> by BINOP_2:def 3;
  hence thesis;
end;

theorem
  (i|->c1) + (i|->c2) = i|->(c1+c2)
proof
  reconsider s1=c1, s2=c2 as Element of COMPLEX by XCMPLX_0:def 2;
  (i|->s1) + (i|->s2) = i|->(addcomplex.(s1,s2)) by FINSEQOP:18
    .= i|->(c1+c2) by BINOP_2:def 3;
  hence thesis;
end;

definition let F;
  redefine func -F -> FinSequence of COMPLEX equals
  compcomplex*F;
  coherence by Lm2;
  compatibility
  proof
    let F1 be FinSequence of COMPLEX;
A1: dom(-F) = dom F by VALUED_1:8;
A2: rng F c= COMPLEX & dom compcomplex = COMPLEX by FUNCT_2:def 1; then
A3: dom(compcomplex*F) = dom F by RELAT_1:46;
    thus F1 = -F implies F1 = compcomplex*F
    proof
      assume A4: F1 = -F;
      now
        let c be set;
        assume A5: c in dom F1;
        thus F1.c = -(F.c) by A4,VALUED_1:8
          .= compcomplex.(F.c) by BINOP_2:def 1
          .= (compcomplex*F).c by A1,A4,A5,FUNCT_1:23;
      end;
      hence thesis by A3,A4,FUNCT_1:9,VALUED_1:8;
    end;
    assume A6: F1 = compcomplex*F;
    now
      let c be set;
      assume A7: c in dom F1;
      thus (-F).c = -(F.c) by VALUED_1:8
        .= compcomplex.(F.c) by BINOP_2:def 1
        .= (compcomplex*F).c by A6,A7,FUNCT_1:22;
    end;
    hence thesis by A1,A2,A6,FUNCT_1:9,RELAT_1:46;
  end;
end;

definition let i,R;
  redefine func -R -> Element of i-tuples_on COMPLEX;
  coherence by FINSEQ_2:133;
end;

theorem
  -<*c*> = <*-c*>
proof
  reconsider s=c as Element of COMPLEX by XCMPLX_0:def 2;
  -<*s*> = <*compcomplex.s*> by FINSEQ_2:39
        .= <*-c*> by BINOP_2:def 1;
  hence thesis;
end;

theorem Th8:
  -(i|->c) = i|->-c
proof
  reconsider s=c as Element of COMPLEX by XCMPLX_0:def 2;
  -(i|->s) = i|->(compcomplex.s) by FINSEQOP:17
          .= i|->-c by BINOP_2:def 1;
  hence thesis;
end;

theorem
  R1 + R = R2 + R implies R1 = R2
proof
  assume R1 + R = R2 + R; then
  R1 + (R + -R)= (R2 + R)+-R by FINSEQOP:29; then
A1: R1 + (R + -R)= R2 + (R + -R) by FINSEQOP:29;
  R + -R = i|->0c by SEQ_4:68,69,BINOP_2:1,FINSEQOP:77; then
  R1 = R2 + (i|->0c) by A1,BINOP_2:1,FINSEQOP:57;
  hence thesis by BINOP_2:1,FINSEQOP:57;
end;

theorem Th10:
  -(F1 + F2) = -F1 + -F2
proof
A1: dom -(F1 + F2) = dom(F1+F2) by VALUED_1:8;
A2: dom(F1+F2) = dom F1 /\ dom F2 by VALUED_1:def 1;
A3: dom (-F1 + -F2) = dom (-F1) /\ dom -F2 by VALUED_1:def 1
    .= dom F1 /\ dom -F2 by VALUED_1:8
    .= dom F1 /\ dom F2 by VALUED_1:8;
  now
    let i;
    assume A4: i in dom -(F1+F2);
    thus (-(F1 + F2)).i = -((F1+F2).i) by VALUED_1:8
    .= -(F1.i+F2.i) by A1,A4,VALUED_1:def 1
    .= -(F1.i)+-(F2.i)
    .= -(F1.i) + (-F2).i by VALUED_1:8
    .= (-F1).i + (-F2).i by VALUED_1:8
    .= (-F1 + -F2).i by A1,A2,A3,A4,VALUED_1:def 1;
  end;
  hence thesis by A2,A3,FINSEQ_1:17,VALUED_1:8;
end;

definition let F1,F2;
  redefine func F1 - F2 -> FinSequence of COMPLEX equals
  diffcomplex.:(F1,F2);
  coherence by Lm2;
  compatibility
  proof
    reconsider F3=F1,F4=F2 as FinSequence of COMPLEX by Lm2;
    let F be FinSequence of COMPLEX;
A1: dom (F1-F2) = dom F1 /\ dom F2 by VALUED_1:12;
    dom diffcomplex = [:COMPLEX,COMPLEX:] by FUNCT_2:def 1; then
A2: [:rng F3, rng F4:] c= dom diffcomplex by ZFMISC_1:119; then
A3: dom(diffcomplex.:(F1,F2)) = dom F1 /\ dom F2 by FUNCOP_1:84;
    thus F = F1-F2 implies F = diffcomplex.:(F1,F2)
    proof
      assume A4: F = F1-F2;
      for z being set st z in dom(diffcomplex.:(F1,F2))
        holds F.z = diffcomplex.(F1.z,F2.z)
      proof
        let z be set;
        assume z in dom(diffcomplex.:(F1,F2));
        hence F.z = F1.z - F2.z by A1,A3,A4,VALUED_1:13
          .= diffcomplex.(F1.z,F2.z) by BINOP_2:def 4;
      end;
      hence thesis by A1,A3,A4,FUNCOP_1:27;
    end;
    assume A5: F = diffcomplex.:(F1,F2);
    now
      let c be set;
      assume c in dom F;
      hence F.c = diffcomplex.(F1.c,F2.c) by A5,FUNCOP_1:28
               .= F1.c - F2.c by BINOP_2:def 4;
    end;
    hence thesis by A1,A2,A5,FUNCOP_1:84,VALUED_1:14;
  end;
end;

definition let i,R1,R2;
  redefine func R1 - R2 -> Element of i-tuples_on COMPLEX;
  coherence by FINSEQ_2:140;
end;

theorem
  (R1-R2).s = R1.s - R2.s
proof
  per cases;
  suppose
A1: not s in Seg i; then
A2: not s in dom R2 by FINSEQ_2:144;
A3: not s in dom R1 by A1,FINSEQ_2:144;
    not s in dom(R1-R2) by A1,FINSEQ_2:144;
    hence (R1-R2).s = 0-0 by FUNCT_1:def 4
      .= R1.s - 0 by A3,FUNCT_1:def 4
      .= R1.s - R2.s by A2,FUNCT_1:def 4;
  end;
  suppose s in Seg i; then
    s in dom (R1 - R2) by FINSEQ_2:144;
    hence thesis by VALUED_1:13;
  end;
end;

theorem
  <*>COMPLEX - F = <*>COMPLEX & F - <*>COMPLEX = <*>COMPLEX
proof
  F is FinSequence of COMPLEX by Lm2;
  hence thesis by FINSEQ_2:87;
end;

theorem
  <*c1*> - <*c2*> = <*c1-c2*>
proof
  reconsider s1=c1, s2=c2 as Element of COMPLEX by XCMPLX_0:def 2;
  <*s1*> - <*s2*> = <*diffcomplex.(s1,s2)*> by FINSEQ_2:88
                 .= <*c1-c2*> by BINOP_2:def 4;
  hence thesis;
end;

theorem
  (i|->c1) - (i|->c2) = i|->(c1-c2)
proof
  reconsider s1=c1, s2=c2 as Element of COMPLEX by XCMPLX_0:def 2;
  (i|->s1) - (i|->s2) = i|->(diffcomplex.(s1,s2)) by FINSEQOP:18
                     .= i|->(c1-c2) by BINOP_2:def 4;
  hence thesis;
end;

theorem
  R - (i|-> 0c) = R
proof
  thus R - (i|-> 0c) = R + (i|->(-0)) by Th8
    .= R by BINOP_2:1,FINSEQOP:57;
end;

theorem
  -(F1 - F2) = F2 - F1
proof
  thus -(F1 - F2) = -F1 + --F2 by Th10
    .= F2 - F1;
end;

theorem
  -(F1 - F2) = -F1 + F2
proof
  thus -(F1 - F2) = -F1 +--F2 by Th10
    .= -F1 + F2;
end;

theorem
  R1 - R2 = i|->0c implies R1 = R2
proof
  assume R1 - R2 = i|->0c; then
  R1 = --R2 by SEQ_4:68,69,BINOP_2:1,FINSEQOP:78;
  hence thesis;
end;

theorem
  R1 = R1 + R - R
proof
  thus R1 = R1 + (i|-> 0c) by BINOP_2:1,FINSEQOP:57
    .= R1 + (R - R) by SEQ_4:68,69,BINOP_2:1,FINSEQOP:77
    .= R1 + R - R by RFUNCT_1:35;
end;

theorem
  R1 = R1 - R + R
proof
  thus R1 = R1 + (i|-> 0c ) by BINOP_2:1,FINSEQOP:57
    .= R1 + (-R + R) by SEQ_4:68,69,BINOP_2:1,FINSEQOP:77
    .= R1 - R + R by FINSEQOP:29;
end;

notation let F,c;
  synonym c*F for c(#)F;
end;

definition let F,c;
  redefine func c*F -> FinSequence of COMPLEX equals
  (c multcomplex)*F;
  coherence by Lm2;
  compatibility
  proof
    let F1 be FinSequence of COMPLEX;
A1: dom(c*F) = dom F by VALUED_1:def 5;
A2: rng F c= COMPLEX & dom(c multcomplex) = COMPLEX by FUNCT_2:def 1; then
A3: dom((c multcomplex)*F) = dom F by RELAT_1:46;
    thus F1 = c*F implies F1 = (c multcomplex)*F
    proof
      assume A4: F1 = c*F;
      now
        let s;
        assume A5: s in dom F1;
        hence F1.s = c*(F.s) by A4,VALUED_1:def 5
          .= (c multcomplex).(F.s) by Lm1
          .= ((c multcomplex)*F).s by A1,A4,A5,FUNCT_1:23;
      end;
      hence thesis by A1,A3,A4,FUNCT_1:9;
    end;
    assume A6: F1 = (c multcomplex)*F;
    now
      let s;
      assume A7: s in dom F1;
      thus (c*F).s = c*(F.s) by VALUED_1:6
        .= (c multcomplex).(F.s) by Lm1
        .= ((c multcomplex)*F).s by A6,A7,FUNCT_1:22;
    end;
    hence thesis by A1,A2,A6,FUNCT_1:9,RELAT_1:46;
  end;
end;

definition let i,R,c;
  redefine func c*R -> Element of i-tuples_on COMPLEX;
  coherence by FINSEQ_2:133;
end;

theorem
  c*<*c1*> = <*c*c1*>
proof
  reconsider s=c, s1=c1 as Element of COMPLEX by XCMPLX_0:def 2;
  s*<*s1*> = <*(multcomplex[;](s,id COMPLEX)).s1*> by FINSEQ_2:39
          .= <*c*c1*> by Lm1;
  hence thesis;
end;

theorem Th22:
  c1*(i|->c2) = i|->(c1*c2)
proof
  reconsider s1=c1, s2=c2 as  Element of COMPLEX by XCMPLX_0:def 2;
  s1*(i|->s2) = i|->((multcomplex[;](s1,id COMPLEX)).s2) by FINSEQOP:17
             .= i|->(c1*c2) by Lm1;
  hence thesis;
end;

theorem
  (c1 + c2)*F = c1*F + c2*F
proof
A1: dom ((c1 + c2)*F) = dom F by VALUED_1:def 5;
A2: dom (c1*F + c2*F) = dom (c1*F) /\ dom (c2*F) by VALUED_1:def 1;
A3: dom (c1*F) = dom F by VALUED_1:def 5;
A4: dom (c2*F) = dom F by VALUED_1:def 5;
    now
      let i;
      assume A5: i in dom ((c1+c2)*F);
      thus ((c1+c2)*F).i = (c1+c2)*(F.i) by VALUED_1:6
      .= c1*(F.i) + c2*(F.i)
      .= c1*(F.i) + (c2*F).i by VALUED_1:6
      .= (c1*F).i + (c2*F).i by VALUED_1:6
      .= (c1*F+c2*F).i by A1,A2,A3,A4,A5,VALUED_1:def 1;
    end;
    hence thesis by A1,A2,A3,A4,FINSEQ_1:17;
end;

theorem
  0c*R = i|->0c
proof
A1: rng R c= COMPLEX;
  thus 0c*R = multcomplex[;](0c,(id COMPLEX)*R) by FUNCOP_1:44
    .= multcomplex[;](0c,R) by A1,RELAT_1:79
    .= i|->0c by SEQ_4:71,68,BINOP_2:1,FINSEQOP:80;
end;

notation let F1,F2;
  synonym mlt(F1,F2) for F1(#)F2;
end;

definition let F1,F2;
  redefine func mlt(F1,F2) -> FinSequence of COMPLEX equals
  multcomplex.:(F1,F2);
  coherence by Lm2;
  compatibility
  proof
    reconsider F3=F1,F4=F2 as FinSequence of COMPLEX by Lm2;
    let F be FinSequence of COMPLEX;
    dom multcomplex = [:COMPLEX,COMPLEX:] by FUNCT_2:def 1; then
    [:rng F3, rng F4:] c= dom multcomplex by ZFMISC_1:119; then
A1: dom(multcomplex.:(F1,F2)) = dom F1 /\ dom F2 by FUNCOP_1:84;
A2: dom mlt(F1,F2) = dom F1 /\ dom F2 by VALUED_1:def 4;
    thus F = mlt(F1,F2) implies F = multcomplex.:(F1,F2)
    proof
      assume A3: F = mlt(F1,F2);
      for z being set st z in dom(multcomplex.:(F1,F2))
        holds F.z = multcomplex.(F1.z,F2.z)
      proof
        let z be set;
        assume z in dom(multcomplex.:(F1,F2));
        thus F.z = F1.z * F2.z by A3,VALUED_1:5
          .= multcomplex.(F1.z,F2.z) by BINOP_2:def 5;
      end;
      hence thesis by A1,A2,A3,FUNCOP_1:27;
    end;
    assume A4: F = multcomplex.:(F1,F2);
    now
      let c be set;
      assume c in dom F;
      hence F.c = multcomplex.(F1.c,F2.c) by A4,FUNCOP_1:28
               .= F1.c * F2.c by BINOP_2:def 5;
    end;
    hence thesis by A1,A4,VALUED_1:def 4;
  end;
  commutativity
  proof
    let F be FinSequence of COMPLEX;
    let F1,F2;
    reconsider F3=F1,F4=F2 as FinSequence of COMPLEX by Lm2;
A5: dom multcomplex = [:COMPLEX,COMPLEX:] by FUNCT_2:def 1; then
A6: [:rng F4, rng F3:] c= dom multcomplex by ZFMISC_1:119;
    [:rng F3, rng F4:] c= dom multcomplex by A5,ZFMISC_1:119; then
A7: dom(multcomplex.:(F1,F2)) = dom F1 /\ dom F2 by FUNCOP_1:84
      .= dom(multcomplex.:(F2,F1)) by A6,FUNCOP_1:84;
    assume A8: F = multcomplex.:(F1,F2);
    for z being set st z in dom(multcomplex.:(F2,F1))
      holds F.z = multcomplex.(F2.z,F1.z)
    proof
      let z be set such that
A9:   z in dom(multcomplex.:(F2,F1));
      set F1z = F1.z, F2z =F2.z;
      thus F.z = multcomplex.(F1.z,F2.z) by A8,A7,A9,FUNCOP_1:28
        .= F1z * F2z by BINOP_2:def 5
        .= multcomplex.(F2.z,F1.z) by BINOP_2:def 5;
    end;
    hence thesis by A8,A7,FUNCOP_1:27;
  end;
end;

definition let i,R1,R2;
  redefine func mlt(R1,R2) -> Element of i-tuples_on COMPLEX;
  coherence by FINSEQ_2:140;
end;

theorem
  mlt(<*>COMPLEX,F) = <*>COMPLEX
proof
  F is FinSequence of COMPLEX by Lm2;
  hence thesis by FINSEQ_2:87;
end;

theorem
  mlt(<*c1*>,<*c2*>) = <*c1*c2*>
proof
  reconsider s1=c1, s2=c2 as Element of COMPLEX by XCMPLX_0:def 2;
  mlt(<*s1*>,<*s2*>) = <*multcomplex.(s1,s2)*> by FINSEQ_2:88
    .= <*c1*c2*> by BINOP_2:def 5;
  hence thesis;
end;

theorem Th27:
  mlt(i|->c,R) = c*R
proof
  reconsider s=c as Element of COMPLEX by XCMPLX_0:def 2;
  mlt(i|->s,R) = multcomplex[;](s,R) by FINSEQOP:21
    .= c*R by FINSEQOP:23;
  hence thesis;
end;

theorem
  mlt(i|->c1,i|->c2) = i|->(c1*c2)
proof
  reconsider s1=c1, s2=c2 as Element of COMPLEX by XCMPLX_0:def 2;
  mlt(i|->s1,i|->s2) = s1*(i|->s2) by Th27
    .= i|->(c1*c2) by Th22;
  hence thesis;
end;

begin :: Finite Sum of Finite Sequence of Complex Numbers

theorem Th29:
  Sum(<*> COMPLEX) = 0c by BINOP_2:1,FINSOP_1:11;

theorem
  Sum <*c*> = c
proof
  reconsider c as Element of COMPLEX by XCMPLX_0:def 2;
  Sum <*c*> = c by FINSOP_1:12;
  hence thesis;
end;

theorem Th31:
  Sum(F^<*c*>) = Sum F + c
proof
  reconsider s=c as Element of COMPLEX by XCMPLX_0:def 2;
  reconsider F1=F as FinSequence of COMPLEX by Lm2;
  thus Sum(F^<*c*>) = Sum(F1^<*s*>)
    .= addcomplex.(addcomplex $$ F1,s) by FINSOP_1:5
    .= Sum F1 + c by BINOP_2:def 3
    .= Sum F + c;
end;

theorem Th32:
  Sum(F1^F2) = Sum F1 + Sum F2
proof
  reconsider F3=F1,F4=F2 as FinSequence of COMPLEX by Lm2;
  thus Sum(F1^F2) = Sum(F3^F4)
    .= addcomplex.(addcomplex $$ F3,addcomplex $$ F4) by FINSOP_1:6
    .= Sum F3 + Sum F4 by BINOP_2:def 3
    .= Sum F1 + Sum F2;
end;

theorem
  Sum(<*c*>^F) = c + Sum F
proof
  reconsider s=c as Element of COMPLEX by XCMPLX_0:def 2;
  thus Sum(<*c*>^F) = Sum <*s*> + Sum F by Th32
    .= c + Sum F by FINSOP_1:12;
end;

theorem Th34:
  Sum<*c1,c2*> = c1 + c2
proof
  reconsider s1=c1 as Element of COMPLEX by XCMPLX_0:def 2;
  thus Sum<*c1,c2*> = Sum<*s1*> + c2 by Th31
    .= c1 + c2 by FINSOP_1:12;
end;

theorem
  Sum<*c1,c2,c3*> = c1 + c2 + c3
proof
  thus Sum<*c1,c2,c3*> = Sum<*c1,c2*> + c3 by Th31
    .= c1 + c2 + c3 by Th34;
end;

theorem Th36:
  Sum(i |-> c) = i*c
proof
  reconsider c as Element of COMPLEX by XCMPLX_0:def 2;
  defpred P[Nat] means Sum($1 |->c) = $1*c;
A1: for i st P[i] holds P[(i+1)]
  proof
    let i such that
A2: Sum(i |-> c) = i*c;
    thus Sum((i+1) |-> c) = Sum((i |-> c)^<*c*>) by FINSEQ_2:74
      .= i*c + 1*c by A2,Th31
      .= (i+1)*c;
  end;
A3: P[0] by Th29;
  for i holds P[i] from NAT_1:sch 2(A3,A1);
  hence thesis;
end;

theorem
  Sum(i |-> 0c) = 0c
proof
  thus Sum(i |-> 0c) = i*0 by Th36
    .= 0c;
end;

theorem
  Sum(c*F) = c*(Sum F)
proof
  reconsider F1=F as FinSequence of COMPLEX by Lm2;
  reconsider s=c as Element of COMPLEX by XCMPLX_0:def 2;
  set cM = multcomplex[;](s,id COMPLEX);
  thus Sum (c*F) = cM.(addcomplex $$ F1) by SEQ_4:71,68,SETWOP_2:41
    .= c*(Sum F1) by Lm1
    .= c*(Sum F);
end;

theorem Th39:
  Sum -F = -(Sum F)
proof
  reconsider F1=F as FinSequence of COMPLEX by Lm2;
  thus Sum -F = compcomplex.(addcomplex $$ F1) by SEQ_4:68,69,SETWOP_2:42
    .= -(Sum F1) by BINOP_2:def 1
    .= -(Sum F);
end;

theorem Th40:
  Sum(R1 + R2) = Sum R1 + Sum R2
proof
  reconsider T1=R1, T2=R2 as Element of i-tuples_on COMPLEX by FINSEQ_2:151;
  thus Sum(R1 + R2) = addcomplex.(addcomplex$$T1,addcomplex$$T2) by SETWOP_2:46
    .= Sum R1 + Sum R2 by BINOP_2:def 3;
end;

theorem
  Sum(R1 - R2) = Sum R1 - Sum R2
proof
  thus Sum(R1 - R2) = Sum R1 + Sum -R2 by Th40
  .= Sum R1 - Sum R2 by Th39;
end;

begin :: The Product of Finite Sequences of Complex Numbers

Lm3: for F being empty FinSequence holds Product F = 1
proof
  Product <*>COMPLEX = 1 by BINOP_2:6,FINSOP_1:11;
  hence thesis;
end;

theorem
  Product <*>COMPLEX = 1 by Lm3;

theorem
  Product (<*c*>^F) = c * Product F
proof
  thus Product (<*c*>^F) = Product <*c*> * Product F by RVSUM_1:127
    .= c * Product F by RVSUM_1:125;
end;

theorem
  for R being Element of 0-tuples_on COMPLEX holds Product R = 1 by Lm3;

theorem
  Product ((i+j) |->c) = (Product (i|->c))*(Product (j|->c))
proof
  reconsider s=c as Element of COMPLEX by XCMPLX_0:def 2;
  Product ((i+j) |->s) =
    multcomplex.(multcomplex$$(i|->s),multcomplex$$(j|->s)) by SETWOP_2:37
    .= (Product (i|->s))*(Product (j|->s)) by BINOP_2:def 5;
  hence thesis;
end;

theorem
  Product ((i*j) |->c) = Product (j |-> (Product (i|->c)))
proof
  reconsider c as Element of COMPLEX by XCMPLX_0:def 2;
  Product ((i*j) |->c) = Product (j |-> (Product (i|->c))) by SETWOP_2:38;
  hence thesis;
end;

theorem
  Product (i|->(c1*c2)) = (Product (i|->c1))*(Product (i|->c2))
proof
  reconsider s1=c1, s2=c2 as Element of COMPLEX by XCMPLX_0:def 2;
  Product (i|->(s1*s2)) = multcomplex$$(i|->multcomplex.(s1,s2))
  by BINOP_2:def 5
    .= multcomplex.(multcomplex$$(i|->s1),multcomplex$$(i|->s2)) by SETWOP_2:47
    .= (Product (i|->s1))*(Product (i|->s2)) by BINOP_2:def 5;
  hence thesis;
end;

theorem Th48:
  Product mlt(R1,R2) = Product R1 * Product R2
proof
  reconsider T1=R1, T2=R2 as Element of i-tuples_on COMPLEX by FINSEQ_2:151;
  thus Product (mlt(R1,R2)) = multcomplex.(multcomplex$$T1,multcomplex$$T2)
  by SETWOP_2:46
    .= Product R1 * Product R2 by BINOP_2:def 5;
end;

theorem
  Product (c*R) = Product (i|->c) * Product R
proof
  reconsider s=c as Element of COMPLEX by XCMPLX_0:def 2;
  thus Product (c*R) = Product mlt(i|->s,R) by Th27
    .= Product (i|->c) * Product R by Th48;
end;

begin :: from EUCLID_2 (partially modified)

theorem
  for x being complex-valued FinSequence holds len (-x)=len x
proof
  let x be complex-valued FinSequence;
  dom (-x)=dom x by VALUED_1:8;
  hence thesis by FINSEQ_3:31;
end;

theorem
  for x1,x2 being complex-valued FinSequence st len x1=len x2 holds
  len (x1+x2)=len x1
proof
  let x1,x2 be complex-valued FinSequence;
  set n=len x1;
A1: x2 is FinSequence of COMPLEX by Lm2;
  x1 is FinSequence of COMPLEX by Lm2; then
  reconsider z1=x1 as Element of (len x1)-tuples_on COMPLEX by FINSEQ_2:110;
  assume len x1=len x2; then
  reconsider z2=x2 as Element of n-tuples_on COMPLEX by A1,FINSEQ_2:110;
  dom (z1+z2)=Seg n by FINSEQ_2:144;
  hence thesis by FINSEQ_1:def 3;
end;

theorem
  for x1,x2 being complex-valued FinSequence st len x1=len x2 holds
  len (x1-x2)=len x1
proof
  let x1,x2 be complex-valued FinSequence;
  set n=len x1;
A1: x2 is FinSequence of COMPLEX by Lm2;
  x1 is FinSequence of COMPLEX by Lm2; then
  reconsider z1=x1 as Element of (len x1)-tuples_on COMPLEX by FINSEQ_2:110;
  assume len x1=len x2; then
  reconsider z2=x2 as Element of n-tuples_on COMPLEX by A1,FINSEQ_2:110;
  dom (z1-z2)=Seg n by FINSEQ_2:144;
  hence thesis by FINSEQ_1:def 3;
end;

theorem
  for a being real number, x being complex-valued FinSequence
  holds len (a*x)=len x
proof
  let a be real number, x be complex-valued FinSequence;
  set n=len x;
  x is FinSequence of COMPLEX by Lm2; then
  reconsider z=x as Element of n-tuples_on COMPLEX by FINSEQ_2:110;
  len (a*z)=n by FINSEQ_1:def 18;
  hence thesis;
end;

theorem
  for x,y,z being complex-valued FinSequence st len x=len y & len y=len z
  holds mlt(x+y,z) = mlt(x,z)+mlt(y,z)
proof
  let x,y,z be complex-valued FinSequence;
A1:x is FinSequence of COMPLEX & y is FinSequence of COMPLEX &
  z is FinSequence of COMPLEX by Lm2;
  assume len x=len y & len y=len z; then
  reconsider x2=x, y2=y, z2=z as Element of (len x)-tuples_on COMPLEX
  by A1,FINSEQ_2:110;
A2: dom (mlt(x+y,z))=Seg len(mlt(x2+y2,z2)) by FINSEQ_1:def 3
    .=Seg len x by FINSEQ_1:def 18
    .=Seg len (mlt(x2,z2)+mlt(y2,z2)) by FINSEQ_1:def 18
    .=dom (mlt(x2,z2)+mlt(y2,z2)) by FINSEQ_1:def 3;
A3: dom (mlt(x,z))=Seg len(mlt(x2,z2)) by FINSEQ_1:def 3
    .=Seg len x by FINSEQ_1:def 18
    .=Seg len (mlt(x2,z2)+mlt(y2,z2)) by FINSEQ_1:def 18
    .=dom (mlt(x2,z2)+mlt(y2,z2)) by FINSEQ_1:def 3;
  for i being Nat st i in dom (mlt(x+y,z)) holds mlt(x+y,z).i=(mlt(x,z)+
  mlt(y,z)).i
  proof
    let i be Nat;
    assume A4: i in dom mlt(x+y,z);
    set a=x.i, b=y.i, d=(x+y).i, e=z.i;
    len (x2+y2)=len x by FINSEQ_1:def 18; then
    dom (x2+y2)=Seg len x by FINSEQ_1:def 3
      .=Seg len(mlt(x2,z2)) by FINSEQ_1:def 18
      .=dom (mlt(x,z)) by FINSEQ_1:def 3; then
A5: d=a+b by A2,A3,A4,VALUED_1:def 1;
    thus mlt(x+y,z).i=d*e by VALUED_1:5
      .=a*e+b*e by A5
      .=mlt(x,z).i +b*e by VALUED_1:5
      .=mlt(x,z).i +mlt(y,z).i by VALUED_1:5
      .=(mlt(x,z)+mlt(y,z)).i by A2,A4,VALUED_1:def 1;
  end;
  hence thesis by A2,FINSEQ_1:17;
end;