:: RVSUM_2 semantic presentation

begin

definition
let F be complex-valued Relation;
:: original: rng
redefine func rng F ->  Subset of COMPLEX;
coherence
 rng F is Subset of COMPLEX 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;
clusterF1 (#) F ->  FinSequence-like ;
coherence
 F * F1 is FinSequence-like
proof
consider n1 being Nat such that
A1: dom F1 = Seg n1 by FINSEQ_1:def_2;
take  n1 ; :: according to FINSEQ_1:def_2 ::_thesis: dom (F * F1) = Seg n1
 ( dom F = COMPLEX & rng F1 c= COMPLEX ) by FUNCT_2:def_1;
hence  dom (F * F1) = Seg n1 by A1, RELAT_1:27; ::_thesis: verum
end;
end;


definition
func sqrcomplex  ->  UnOp of COMPLEX means :Def1: :: RVSUM_2:def 1
 for c being complex number holds it . c = c ^2 ;
existence
 ex b1 being UnOp of COMPLEX st
for c being complex number holds b1 . c = c ^2
proof
deffunc H1( Element of COMPLEX ) ->  Element of COMPLEX = $1 ^2 ;
consider G being Function of COMPLEX,COMPLEX such that
A1: for x being Element of COMPLEX holds G . x = H1(x) from FUNCT_2:sch_4();
take  G ; ::_thesis: for c being complex number holds G . c = c ^2
let c be complex number ; ::_thesis: G . c = c ^2
 c in COMPLEX by XCMPLX_0:def_2;
hence  G . c = c ^2 by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being UnOp of COMPLEX st ( for c being complex number holds b1 . c = c ^2 ) & ( for c being complex number holds b2 . c = c ^2 ) holds
b1 = b2
proof
let G1, G2 be UnOp of COMPLEX; ::_thesis: ( ( for c being complex number holds G1 . c = c ^2 ) & ( for c being complex number holds G2 . c = c ^2 ) implies G1 = G2 )
assume that
A2: for c being complex number holds G1 . c = c ^2 and
A3: for c being complex number holds G2 . c = c ^2 ; ::_thesis: G1 = G2
now__::_thesis:_for_x_being_Element_of_COMPLEX_holds_G1_._x_=_G2_._x
let x be Element of COMPLEX ; ::_thesis: G1 . x = G2 . x
 G1 . x = x ^2 by A2;
hence  G1 . x = G2 . x by A3; ::_thesis: verum
end;
hence  G1 = G2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines sqrcomplex RVSUM_2:def_1_:_
 for b1 being UnOp of COMPLEX holds
( b1 = sqrcomplex iff for c being complex number holds b1 . c = c ^2 );

theorem :: RVSUM_2:1
sqrcomplex is_distributive_wrt multcomplex
proof
let x1 be Element of COMPLEX ; :: according to BINOP_1:def_20 ::_thesis: for b1 being Element of COMPLEX holds sqrcomplex . (multcomplex . (x1,b1)) = multcomplex . ((sqrcomplex . x1),(sqrcomplex . b1))
let x2 be Element of COMPLEX ; ::_thesis: sqrcomplex . (multcomplex . (x1,x2)) = multcomplex . ((sqrcomplex . x1),(sqrcomplex . 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 ; ::_thesis: verum
end;

Lm1:  for c, c1 being complex number holds (multcomplex [;] (c,(id COMPLEX))) . c1 = c * c1
proof
let c, c1 be complex number ; ::_thesis: (multcomplex [;] (c,(id COMPLEX))) . c1 = c * c1
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:53
.= multcomplex . (a,s) by FUNCT_1:18
.= c * c1 by BINOP_2:def_5 ; ::_thesis: verum
end;

theorem :: RVSUM_2:2
for c being complex number holds c multcomplex is_distributive_wrt addcomplex
proof
let c be complex number ; ::_thesis: c multcomplex is_distributive_wrt addcomplex
 c in COMPLEX by XCMPLX_0:def_2;
hence  c multcomplex is_distributive_wrt addcomplex by FINSEQOP:54, SEQ_4:54; ::_thesis: verum
end;

begin

Lm2:  for F being complex-valued FinSequence holds F is FinSequence of COMPLEX
proof
let F be complex-valued FinSequence; ::_thesis: F is FinSequence of COMPLEX
thus  rng F c= COMPLEX ; :: according to FINSEQ_1:def_4 ::_thesis: verum
end;

definition
let F1, F2 be complex-valued FinSequence;
:: original: +
redefine funcF1 + F2 ->  FinSequence of COMPLEX  equals :: RVSUM_2:def 2
addcomplex .: (F1,F2);
coherence
 F1 + F2 is FinSequence of COMPLEX by Lm2;
compatibility
 for b1 being FinSequence of COMPLEX holds
( b1 = F1 + F2 iff b1 = addcomplex .: (F1,F2) )
proof
reconsider F3 = F1, F4 = F2 as FinSequence of COMPLEX by Lm2;
let F be FinSequence of COMPLEX ; ::_thesis: ( F = F1 + F2 iff F = addcomplex .: (F1,F2) )
 dom addcomplex = [:COMPLEX,COMPLEX:] by FUNCT_2:def_1;
then  [:(rng F3),(rng F4):] c= dom addcomplex by ZFMISC_1:96;
then A1: dom (addcomplex .: (F1,F2)) = (dom F1) /\ (dom F2) by FUNCOP_1:69;
A2: dom (F1 + F2) = (dom F1) /\ (dom F2) by VALUED_1:def_1;
thus  ( F = F1 + F2 implies F = addcomplex .: (F1,F2) ) ::_thesis: ( F = addcomplex .: (F1,F2) implies F = F1 + F2 )
proof
assume A3: F = F1 + F2 ; ::_thesis: F = addcomplex .: (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 ; ::_thesis: ( z in dom (addcomplex .: (F1,F2)) implies F . z = addcomplex . ((F1 . z),(F2 . z)) )
assume  z in dom (addcomplex .: (F1,F2)) ; ::_thesis: F . z = addcomplex . ((F1 . z),(F2 . z))
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 ;
::_thesis: verum
end;
hence  F = addcomplex .: (F1,F2) by A2, A1, A3, FUNCOP_1:21; ::_thesis: verum
end;
assume A4: F = addcomplex .: (F1,F2) ; ::_thesis: F = F1 + F2
now__::_thesis:_for_c_being_set_st_c_in_dom_F_holds_
F_._c_=_(F1_._c)_+_(F2_._c)
let c be set ; ::_thesis: ( c in dom F implies F . c = (F1 . c) + (F2 . c) )
assume  c in dom F ; ::_thesis: F . c = (F1 . c) + (F2 . c)
hence F . c = addcomplex . ((F1 . c),(F2 . c)) by A4, FUNCOP_1:22
.= (F1 . c) + (F2 . c) by BINOP_2:def_3 ;
::_thesis: verum
end;
hence  F = F1 + F2 by A1, A4, VALUED_1:def_1; ::_thesis: verum
end;
commutativity
 for b1 being FinSequence of COMPLEX
for F1, F2 being complex-valued FinSequence st b1 = addcomplex .: (F1,F2) holds
b1 = addcomplex .: (F2,F1)
proof
let F be FinSequence of COMPLEX ; ::_thesis: for F1, F2 being complex-valued FinSequence st F = addcomplex .: (F1,F2) holds
F = addcomplex .: (F2,F1)
let F1, F2 be complex-valued FinSequence; ::_thesis: ( F = addcomplex .: (F1,F2) implies F = addcomplex .: (F2,F1) )
assume A5: F = addcomplex .: (F1,F2) ; ::_thesis: F = addcomplex .: (F2,F1)
reconsider F1 = F1, F2 = 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:96;
 [:(rng F1),(rng F2):] c= dom addcomplex by A6, ZFMISC_1:96;
then A8: dom (addcomplex .: (F1,F2)) = (dom F1) /\ (dom F2) by FUNCOP_1:69
.= dom (addcomplex .: (F2,F1)) by A7, FUNCOP_1:69 ;
 for z being set st z in dom (addcomplex .: (F2,F1)) holds
F . z = addcomplex . ((F2 . z),(F1 . z))
proof
let z be set ; ::_thesis: ( z in dom (addcomplex .: (F2,F1)) implies F . z = addcomplex . ((F2 . z),(F1 . z)) )
assume  z in dom (addcomplex .: (F2,F1)) ; ::_thesis: F . z = addcomplex . ((F2 . z),(F1 . z))
hence F . z = addcomplex . ((F1 . z),(F2 . z)) by A5, A8, FUNCOP_1:22
.= (F1 . z) + (F2 . z) by BINOP_2:def_3
.= addcomplex . ((F2 . z),(F1 . z)) by BINOP_2:def_3 ;
::_thesis: verum
end;
hence  F = addcomplex .: (F2,F1) by A5, A8, FUNCOP_1:21; ::_thesis: verum
end;
end;

:: deftheorem  defines + RVSUM_2:def_2_:_
 for F1, F2 being complex-valued FinSequence holds F1 + F2 = addcomplex .: (F1,F2);

definition
let i be Nat;
let R1, R2 be i -element FinSequence of COMPLEX ;
:: original: +
redefine funcR1 + R2 ->  Element of i -tuples_on COMPLEX;
coherence
 R1 + R2 is Element of i -tuples_on COMPLEX by FINSEQ_2:120;
end;

theorem :: RVSUM_2:3
for s being set
for i being Nat
for R1, R2 being b2 -element FinSequence of COMPLEX holds (R1 + R2) . s = (R1 . s) + (R2 . s)
proof
let s be set ; ::_thesis: for i being Nat
for R1, R2 being b1 -element FinSequence of COMPLEX holds (R1 + R2) . s = (R1 . s) + (R2 . s)
let i be Nat; ::_thesis: for R1, R2 being i -element FinSequence of COMPLEX holds (R1 + R2) . s = (R1 . s) + (R2 . s)
let R1, R2 be i -element FinSequence of COMPLEX ; ::_thesis: (R1 + R2) . s = (R1 . s) + (R2 . s)
percases ( not s in Seg i or s in Seg i ) ;
supposeA1: not s in Seg i ; ::_thesis: (R1 + R2) . s = (R1 . s) + (R2 . s)
then A2: not s in dom R2 by FINSEQ_2:124;
A3: not s in dom R1 by A1, FINSEQ_2:124;
 not s in dom (R1 + R2) by A1, FINSEQ_2:124;
hence (R1 + R2) . s = 0 + 0 by FUNCT_1:def_2
.= (R1 . s) + 0 by A3, FUNCT_1:def_2
.= (R1 . s) + (R2 . s) by A2, FUNCT_1:def_2 ;
::_thesis: verum
end;
suppose s in Seg i ; ::_thesis: (R1 + R2) . s = (R1 . s) + (R2 . s)
then  s in dom (R1 + R2) by FINSEQ_2:124;
hence  (R1 + R2) . s = (R1 . s) + (R2 . s) by VALUED_1:def_1; ::_thesis: verum
end;
end;
end;

theorem :: RVSUM_2:4
for F being complex-valued FinSequence holds (<*> COMPLEX) + F = <*> COMPLEX
proof
let F be complex-valued FinSequence; ::_thesis: (<*> COMPLEX) + F = <*> COMPLEX
 F is FinSequence of COMPLEX by Lm2;
hence  (<*> COMPLEX) + F = <*> COMPLEX by FINSEQ_2:73; ::_thesis: verum
end;

theorem :: RVSUM_2:5
for c1, c2 being complex number holds <*c1*> + <*c2*> = <*(c1 + c2)*>
proof
let c1, c2 be complex number ; ::_thesis: <*c1*> + <*c2*> = <*(c1 + c2)*>
reconsider s1 = c1, s2 = c2 as Element of COMPLEX by XCMPLX_0:def_2;
<*s1*> + <*s2*> = <*(addcomplex . (s1,s2))*> by FINSEQ_2:74
.= <*(c1 + c2)*> by BINOP_2:def_3 ;
hence  <*c1*> + <*c2*> = <*(c1 + c2)*> ; ::_thesis: verum
end;

theorem :: RVSUM_2:6
for i being Nat
for c1, c2 being complex number holds (i |-> c1) + (i |-> c2) = i |-> (c1 + c2)
proof
let i be Nat; ::_thesis: for c1, c2 being complex number holds (i |-> c1) + (i |-> c2) = i |-> (c1 + c2)
let c1, c2 be complex number ; ::_thesis: (i |-> c1) + (i |-> c2) = i |-> (c1 + c2)
reconsider s1 = c1, s2 = c2 as Element of COMPLEX by XCMPLX_0:def_2;
(i |-> s1) + (i |-> s2) = i |-> (addcomplex . (s1,s2)) by FINSEQOP:17
.= i |-> (c1 + c2) by BINOP_2:def_3 ;
hence  (i |-> c1) + (i |-> c2) = i |-> (c1 + c2) ; ::_thesis: verum
end;

definition
let F be complex-valued FinSequence;
:: original: -
redefine func - F ->  FinSequence of COMPLEX  equals :: RVSUM_2:def 3
compcomplex * F;
coherence
 - F is FinSequence of COMPLEX by Lm2;
compatibility
 for b1 being FinSequence of COMPLEX holds
( b1 = - F iff b1 = compcomplex * F )
proof
let F1 be FinSequence of COMPLEX ; ::_thesis: ( F1 = - F iff F1 = compcomplex * F )
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:27;
thus  ( F1 = - F implies F1 = compcomplex * F ) ::_thesis: ( F1 = compcomplex * F implies F1 = - F )
proof
assume A4: F1 = - F ; ::_thesis: F1 = compcomplex * F
now__::_thesis:_for_c_being_set_st_c_in_dom_F1_holds_
F1_._c_=_(compcomplex_*_F)_._c
let c be set ; ::_thesis: ( c in dom F1 implies F1 . c = (compcomplex * F) . c )
assume A5: c in dom F1 ; ::_thesis: F1 . c = (compcomplex * F) . c
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:13 ; ::_thesis: verum
end;
hence  F1 = compcomplex * F by A3, A4, FUNCT_1:2, VALUED_1:8; ::_thesis: verum
end;
assume A6: F1 = compcomplex * F ; ::_thesis: F1 = - F
now__::_thesis:_for_c_being_set_st_c_in_dom_F1_holds_
(-_F)_._c_=_(compcomplex_*_F)_._c
let c be set ; ::_thesis: ( c in dom F1 implies (- F) . c = (compcomplex * F) . c )
assume A7: c in dom F1 ; ::_thesis: (- F) . c = (compcomplex * F) . c
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:12 ; ::_thesis: verum
end;
hence  F1 = - F by A1, A2, A6, FUNCT_1:2, RELAT_1:27; ::_thesis: verum
end;
end;

:: deftheorem  defines - RVSUM_2:def_3_:_
 for F being complex-valued FinSequence holds - F = compcomplex * F;

definition
let i be Nat;
let R be i -element FinSequence of COMPLEX ;
:: original: -
redefine func - R ->  Element of i -tuples_on COMPLEX;
coherence
 - R is Element of i -tuples_on COMPLEX by FINSEQ_2:113;
end;

theorem :: RVSUM_2:7
for c being complex number holds - <*c*> = <*(- c)*>
proof
let c be complex number ; ::_thesis: - <*c*> = <*(- c)*>
reconsider s = c as Element of COMPLEX by XCMPLX_0:def_2;
- <*s*> = <*(compcomplex . s)*> by FINSEQ_2:35
.= <*(- c)*> by BINOP_2:def_1 ;
hence  - <*c*> = <*(- c)*> ; ::_thesis: verum
end;

theorem Th8: :: RVSUM_2:8
for i being Nat
for c being complex number holds - (i |-> c) = i |-> (- c)
proof
let i be Nat; ::_thesis: for c being complex number holds - (i |-> c) = i |-> (- c)
let c be complex number ; ::_thesis: - (i |-> c) = i |-> (- c)
reconsider s = c as Element of COMPLEX by XCMPLX_0:def_2;
- (i |-> s) = i |-> (compcomplex . s) by FINSEQOP:16
.= i |-> (- c) by BINOP_2:def_1 ;
hence  - (i |-> c) = i |-> (- c) ; ::_thesis: verum
end;

theorem :: RVSUM_2:9
for i being Nat
for R1, R, R2 being b1 -element FinSequence of COMPLEX st R1 + R = R2 + R holds
R1 = R2
proof
let i be Nat; ::_thesis: for R1, R, R2 being i -element FinSequence of COMPLEX st R1 + R = R2 + R holds
R1 = R2
let R1, R, R2 be i -element FinSequence of COMPLEX ; ::_thesis: ( R1 + R = R2 + R implies R1 = R2 )
assume  R1 + R = R2 + R ; ::_thesis: R1 = R2
then  R1 + (R + (- R)) = (R2 + R) + (- R) by FINSEQOP:28;
then A1: R1 + (R + (- R)) = R2 + (R + (- R)) by FINSEQOP:28;
 R + (- R) = i |-> 0c by BINOP_2:1, FINSEQOP:73, SEQ_4:51, SEQ_4:52;
then  R1 = R2 + (i |-> 0c) by A1, BINOP_2:1, FINSEQOP:56;
hence  R1 = R2 by BINOP_2:1, FINSEQOP:56; ::_thesis: verum
end;

theorem Th10: :: RVSUM_2:10
for F1, F2 being complex-valued FinSequence holds - (F1 + F2) = (- F1) + (- F2)
proof
let F1, F2 be complex-valued FinSequence; ::_thesis: - (F1 + F2) = (- F1) + (- F2)
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__::_thesis:_for_i_being_Nat_st_i_in_dom_(-_(F1_+_F2))_holds_
(-_(F1_+_F2))_._i_=_((-_F1)_+_(-_F2))_._i
let i be Nat; ::_thesis: ( i in dom (- (F1 + F2)) implies (- (F1 + F2)) . i = ((- F1) + (- F2)) . i )
assume A4: i in dom (- (F1 + F2)) ; ::_thesis: (- (F1 + F2)) . i = ((- F1) + (- F2)) . i
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 ; ::_thesis: verum
end;
hence  - (F1 + F2) = (- F1) + (- F2) by A2, A3, FINSEQ_1:13, VALUED_1:8; ::_thesis: verum
end;

definition
let F1, F2 be complex-valued FinSequence;
:: original: -
redefine funcF1 - F2 ->  FinSequence of COMPLEX  equals :: RVSUM_2:def 4
diffcomplex .: (F1,F2);
coherence
 F1 - F2 is FinSequence of COMPLEX by Lm2;
compatibility
 for b1 being FinSequence of COMPLEX holds
( b1 = F1 - F2 iff b1 = diffcomplex .: (F1,F2) )
proof
reconsider F3 = F1, F4 = F2 as FinSequence of COMPLEX by Lm2;
let F be FinSequence of COMPLEX ; ::_thesis: ( F = F1 - F2 iff F = diffcomplex .: (F1,F2) )
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:96;
then A3: dom (diffcomplex .: (F1,F2)) = (dom F1) /\ (dom F2) by FUNCOP_1:69;
thus  ( F = F1 - F2 implies F = diffcomplex .: (F1,F2) ) ::_thesis: ( F = diffcomplex .: (F1,F2) implies F = F1 - F2 )
proof
assume A4: F = F1 - F2 ; ::_thesis: F = diffcomplex .: (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 ; ::_thesis: ( z in dom (diffcomplex .: (F1,F2)) implies F . z = diffcomplex . ((F1 . z),(F2 . z)) )
assume  z in dom (diffcomplex .: (F1,F2)) ; ::_thesis: F . z = diffcomplex . ((F1 . z),(F2 . z))
hence F . z = (F1 . z) - (F2 . z) by A1, A3, A4, VALUED_1:13
.= diffcomplex . ((F1 . z),(F2 . z)) by BINOP_2:def_4 ;
::_thesis: verum
end;
hence  F = diffcomplex .: (F1,F2) by A1, A3, A4, FUNCOP_1:21; ::_thesis: verum
end;
assume A5: F = diffcomplex .: (F1,F2) ; ::_thesis: F = F1 - F2
now__::_thesis:_for_c_being_set_st_c_in_dom_F_holds_
F_._c_=_(F1_._c)_-_(F2_._c)
let c be set ; ::_thesis: ( c in dom F implies F . c = (F1 . c) - (F2 . c) )
assume  c in dom F ; ::_thesis: F . c = (F1 . c) - (F2 . c)
hence F . c = diffcomplex . ((F1 . c),(F2 . c)) by A5, FUNCOP_1:22
.= (F1 . c) - (F2 . c) by BINOP_2:def_4 ;
::_thesis: verum
end;
hence  F = F1 - F2 by A1, A2, A5, FUNCOP_1:69, VALUED_1:14; ::_thesis: verum
end;
end;

:: deftheorem  defines - RVSUM_2:def_4_:_
 for F1, F2 being complex-valued FinSequence holds F1 - F2 = diffcomplex .: (F1,F2);

definition
let i be Nat;
let R1, R2 be i -element FinSequence of COMPLEX ;
:: original: -
redefine funcR1 - R2 ->  Element of i -tuples_on COMPLEX;
coherence
 R1 - R2 is Element of i -tuples_on COMPLEX by FINSEQ_2:120;
end;

theorem :: RVSUM_2:11
for s being set
for i being Nat
for R1, R2 being b2 -element FinSequence of COMPLEX holds (R1 - R2) . s = (R1 . s) - (R2 . s)
proof
let s be set ; ::_thesis: for i being Nat
for R1, R2 being b1 -element FinSequence of COMPLEX holds (R1 - R2) . s = (R1 . s) - (R2 . s)
let i be Nat; ::_thesis: for R1, R2 being i -element FinSequence of COMPLEX holds (R1 - R2) . s = (R1 . s) - (R2 . s)
let R1, R2 be i -element FinSequence of COMPLEX ; ::_thesis: (R1 - R2) . s = (R1 . s) - (R2 . s)
percases ( not s in Seg i or s in Seg i ) ;
supposeA1: not s in Seg i ; ::_thesis: (R1 - R2) . s = (R1 . s) - (R2 . s)
then A2: not s in dom R2 by FINSEQ_2:124;
A3: not s in dom R1 by A1, FINSEQ_2:124;
 not s in dom (R1 - R2) by A1, FINSEQ_2:124;
hence (R1 - R2) . s = 0 - 0 by FUNCT_1:def_2
.= (R1 . s) - 0 by A3, FUNCT_1:def_2
.= (R1 . s) - (R2 . s) by A2, FUNCT_1:def_2 ;
::_thesis: verum
end;
suppose s in Seg i ; ::_thesis: (R1 - R2) . s = (R1 . s) - (R2 . s)
then  s in dom (R1 - R2) by FINSEQ_2:124;
hence  (R1 - R2) . s = (R1 . s) - (R2 . s) by VALUED_1:13; ::_thesis: verum
end;
end;
end;

theorem :: RVSUM_2:12
for F being complex-valued FinSequence holds
( (<*> COMPLEX) - F = <*> COMPLEX & F - (<*> COMPLEX) = <*> COMPLEX )
proof
let F be complex-valued FinSequence; ::_thesis: ( (<*> COMPLEX) - F = <*> COMPLEX & F - (<*> COMPLEX) = <*> COMPLEX )
 F is FinSequence of COMPLEX by Lm2;
hence  ( (<*> COMPLEX) - F = <*> COMPLEX & F - (<*> COMPLEX) = <*> COMPLEX ) by FINSEQ_2:73; ::_thesis: verum
end;

theorem :: RVSUM_2:13
for c1, c2 being complex number holds <*c1*> - <*c2*> = <*(c1 - c2)*>
proof
let c1, c2 be complex number ; ::_thesis: <*c1*> - <*c2*> = <*(c1 - c2)*>
reconsider s1 = c1, s2 = c2 as Element of COMPLEX by XCMPLX_0:def_2;
<*s1*> - <*s2*> = <*(diffcomplex . (s1,s2))*> by FINSEQ_2:74
.= <*(c1 - c2)*> by BINOP_2:def_4 ;
hence  <*c1*> - <*c2*> = <*(c1 - c2)*> ; ::_thesis: verum
end;

theorem :: RVSUM_2:14
for i being Nat
for c1, c2 being complex number holds (i |-> c1) - (i |-> c2) = i |-> (c1 - c2)
proof
let i be Nat; ::_thesis: for c1, c2 being complex number holds (i |-> c1) - (i |-> c2) = i |-> (c1 - c2)
let c1, c2 be complex number ; ::_thesis: (i |-> c1) - (i |-> c2) = i |-> (c1 - c2)
reconsider s1 = c1, s2 = c2 as Element of COMPLEX by XCMPLX_0:def_2;
(i |-> s1) - (i |-> s2) = i |-> (diffcomplex . (s1,s2)) by FINSEQOP:17
.= i |-> (c1 - c2) by BINOP_2:def_4 ;
hence  (i |-> c1) - (i |-> c2) = i |-> (c1 - c2) ; ::_thesis: verum
end;

theorem :: RVSUM_2:15
for i being Nat
for R being b1 -element FinSequence of COMPLEX holds R - (i |-> 0c) = R
proof
let i be Nat; ::_thesis: for R being i -element FinSequence of COMPLEX holds R - (i |-> 0c) = R
let R be i -element FinSequence of COMPLEX ; ::_thesis: R - (i |-> 0c) = R
thus R - (i |-> 0c) = R + (i |-> (- 0)) by Th8
.= R by BINOP_2:1, FINSEQOP:56 ; ::_thesis: verum
end;

theorem :: RVSUM_2:16
for F1, F2 being complex-valued FinSequence holds - (F1 - F2) = F2 - F1
proof
let F1, F2 be complex-valued FinSequence; ::_thesis: - (F1 - F2) = F2 - F1
thus  - (F1 - F2) = (- F1) + (- (- F2)) by Th10
.= F2 - F1 ; ::_thesis: verum
end;

theorem :: RVSUM_2:17
for F1, F2 being complex-valued FinSequence holds - (F1 - F2) = (- F1) + F2
proof
let F1, F2 be complex-valued FinSequence; ::_thesis: - (F1 - F2) = (- F1) + F2
thus  - (F1 - F2) = (- F1) + (- (- F2)) by Th10
.= (- F1) + F2 ; ::_thesis: verum
end;

theorem :: RVSUM_2:18
for i being Nat
for R1, R2 being b1 -element FinSequence of COMPLEX st R1 - R2 = i |-> 0c holds
R1 = R2
proof
let i be Nat; ::_thesis: for R1, R2 being i -element FinSequence of COMPLEX st R1 - R2 = i |-> 0c holds
R1 = R2
let R1, R2 be i -element FinSequence of COMPLEX ; ::_thesis: ( R1 - R2 = i |-> 0c implies R1 = R2 )
assume  R1 - R2 = i |-> 0c ; ::_thesis: R1 = R2
then  R1 = - (- R2) by BINOP_2:1, FINSEQOP:74, SEQ_4:51, SEQ_4:52;
hence  R1 = R2 ; ::_thesis: verum
end;

theorem :: RVSUM_2:19
for i being Nat
for R1, R being b1 -element FinSequence of COMPLEX holds R1 = (R1 + R) - R
proof
let i be Nat; ::_thesis: for R1, R being i -element FinSequence of COMPLEX holds R1 = (R1 + R) - R
let R1, R be i -element FinSequence of COMPLEX ; ::_thesis: R1 = (R1 + R) - R
thus R1 = R1 + (i |-> 0c) by BINOP_2:1, FINSEQOP:56
.= R1 + (R - R) by BINOP_2:1, FINSEQOP:73, SEQ_4:51, SEQ_4:52
.= (R1 + R) - R by RFUNCT_1:23 ; ::_thesis: verum
end;

theorem :: RVSUM_2:20
for i being Nat
for R1, R being b1 -element FinSequence of COMPLEX holds R1 = (R1 - R) + R
proof
let i be Nat; ::_thesis: for R1, R being i -element FinSequence of COMPLEX holds R1 = (R1 - R) + R
let R1, R be i -element FinSequence of COMPLEX ; ::_thesis: R1 = (R1 - R) + R
thus R1 = R1 + (i |-> 0c) by BINOP_2:1, FINSEQOP:56
.= R1 + ((- R) + R) by BINOP_2:1, FINSEQOP:73, SEQ_4:51, SEQ_4:52
.= (R1 - R) + R by FINSEQOP:28 ; ::_thesis: verum
end;

notation
let F be complex-valued FinSequence;
let c be complex number ;
synonym c * F for c (#) F;
end;

definition
let F be complex-valued FinSequence;
let c be complex number ;
:: original: *
redefine funcc * F ->  FinSequence of COMPLEX  equals :: RVSUM_2:def 5
(c multcomplex) * F;
coherence
 c * F is FinSequence of COMPLEX by Lm2;
compatibility
 for b1 being FinSequence of COMPLEX holds
( b1 = c * F iff b1 = (c multcomplex) * F )
proof
let F1 be FinSequence of COMPLEX ; ::_thesis: ( F1 = c * F iff F1 = (c multcomplex) * F )
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:27;
thus  ( F1 = c * F implies F1 = (c multcomplex) * F ) ::_thesis: ( F1 = (c multcomplex) * F implies F1 = c * F )
proof
assume A4: F1 = c * F ; ::_thesis: F1 = (c multcomplex) * F
now__::_thesis:_for_s_being_set_st_s_in_dom_F1_holds_
F1_._s_=_((c_multcomplex)_*_F)_._s
let s be set ; ::_thesis: ( s in dom F1 implies F1 . s = ((c multcomplex) * F) . s )
assume A5: s in dom F1 ; ::_thesis: F1 . s = ((c multcomplex) * F) . s
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:13 ;
::_thesis: verum
end;
hence  F1 = (c multcomplex) * F by A1, A3, A4, FUNCT_1:2; ::_thesis: verum
end;
assume A6: F1 = (c multcomplex) * F ; ::_thesis: F1 = c * F
now__::_thesis:_for_s_being_set_st_s_in_dom_F1_holds_
(c_*_F)_._s_=_((c_multcomplex)_*_F)_._s
let s be set ; ::_thesis: ( s in dom F1 implies (c * F) . s = ((c multcomplex) * F) . s )
assume A7: s in dom F1 ; ::_thesis: (c * F) . s = ((c multcomplex) * F) . s
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:12 ; ::_thesis: verum
end;
hence  F1 = c * F by A1, A2, A6, FUNCT_1:2, RELAT_1:27; ::_thesis: verum
end;
end;

:: deftheorem  defines * RVSUM_2:def_5_:_
 for F being complex-valued FinSequence
for c being complex number holds c * F = (c multcomplex) * F;

definition
let i be Nat;
let R be i -element FinSequence of COMPLEX ;
let c be complex number ;
:: original: *
redefine funcc * R ->  Element of i -tuples_on COMPLEX;
coherence
 c * R is Element of i -tuples_on COMPLEX by FINSEQ_2:113;
end;

theorem :: RVSUM_2:21
for c, c1 being complex number holds c * <*c1*> = <*(c * c1)*>
proof
let c, c1 be complex number ; ::_thesis: c * <*c1*> = <*(c * c1)*>
reconsider s = c, s1 = c1 as Element of COMPLEX by XCMPLX_0:def_2;
s * <*s1*> = <*((multcomplex [;] (s,(id COMPLEX))) . s1)*> by FINSEQ_2:35
.= <*(c * c1)*> by Lm1 ;
hence  c * <*c1*> = <*(c * c1)*> ; ::_thesis: verum
end;

theorem Th22: :: RVSUM_2:22
for i being Nat
for c1, c2 being complex number holds c1 * (i |-> c2) = i |-> (c1 * c2)
proof
let i be Nat; ::_thesis: for c1, c2 being complex number holds c1 * (i |-> c2) = i |-> (c1 * c2)
let c1, c2 be complex number ; ::_thesis: c1 * (i |-> c2) = i |-> (c1 * c2)
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:16
.= i |-> (c1 * c2) by Lm1 ;
hence  c1 * (i |-> c2) = i |-> (c1 * c2) ; ::_thesis: verum
end;

theorem :: RVSUM_2:23
for c1, c2 being complex number
for F being complex-valued FinSequence holds (c1 + c2) * F = (c1 * F) + (c2 * F)
proof
let c1, c2 be complex number ; ::_thesis: for F being complex-valued FinSequence holds (c1 + c2) * F = (c1 * F) + (c2 * F)
let F be complex-valued FinSequence; ::_thesis: (c1 + c2) * F = (c1 * F) + (c2 * F)
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__::_thesis:_for_i_being_Nat_st_i_in_dom_((c1_+_c2)_*_F)_holds_
((c1_+_c2)_*_F)_._i_=_((c1_*_F)_+_(c2_*_F))_._i
let i be Nat; ::_thesis: ( i in dom ((c1 + c2) * F) implies ((c1 + c2) * F) . i = ((c1 * F) + (c2 * F)) . i )
assume A5: i in dom ((c1 + c2) * F) ; ::_thesis: ((c1 + c2) * F) . i = ((c1 * F) + (c2 * F)) . i
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 ; ::_thesis: verum
end;
hence  (c1 + c2) * F = (c1 * F) + (c2 * F) by A1, A2, A3, A4, FINSEQ_1:13; ::_thesis: verum
end;

theorem :: RVSUM_2:24
for i being Nat
for R being b1 -element FinSequence of COMPLEX holds 0c * R = i |-> 0c
proof
let i be Nat; ::_thesis: for R being i -element FinSequence of COMPLEX holds 0c * R = i |-> 0c
let R be i -element FinSequence of COMPLEX ; ::_thesis: 0c * R = i |-> 0c
A1: rng R c= COMPLEX ;
thus 0c * R = multcomplex [;] (0c,((id COMPLEX) * R)) by FUNCOP_1:34
.= multcomplex [;] (0c,R) by A1, RELAT_1:53
.= i |-> 0c by BINOP_2:1, FINSEQOP:76, SEQ_4:51, SEQ_4:54 ; ::_thesis: verum
end;

notation
let F1, F2 be complex-valued FinSequence;
synonym  mlt (F1,F2) for F1 (#) F2;
end;

definition
let F1, F2 be complex-valued FinSequence;
:: original: mlt
redefine func mlt (F1,F2) ->  FinSequence of COMPLEX  equals :: RVSUM_2:def 6
multcomplex .: (F1,F2);
coherence
 mlt (F1,F2) is FinSequence of COMPLEX by Lm2;
compatibility
 for b1 being FinSequence of COMPLEX holds
( b1 = mlt (F1,F2) iff b1 = multcomplex .: (F1,F2) )
proof
reconsider F3 = F1, F4 = F2 as FinSequence of COMPLEX by Lm2;
let F be FinSequence of COMPLEX ; ::_thesis: ( F = mlt (F1,F2) iff F = multcomplex .: (F1,F2) )
 dom multcomplex = [:COMPLEX,COMPLEX:] by FUNCT_2:def_1;
then  [:(rng F3),(rng F4):] c= dom multcomplex by ZFMISC_1:96;
then A1: dom (multcomplex .: (F1,F2)) = (dom F1) /\ (dom F2) by FUNCOP_1:69;
A2: dom (mlt (F1,F2)) = (dom F1) /\ (dom F2) by VALUED_1:def_4;
thus  ( F = mlt (F1,F2) implies F = multcomplex .: (F1,F2) ) ::_thesis: ( F = multcomplex .: (F1,F2) implies F = mlt (F1,F2) )
proof
assume A3: F = mlt (F1,F2) ; ::_thesis: F = multcomplex .: (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 ; ::_thesis: ( z in dom (multcomplex .: (F1,F2)) implies F . z = multcomplex . ((F1 . z),(F2 . z)) )
assume  z in dom (multcomplex .: (F1,F2)) ; ::_thesis: F . z = multcomplex . ((F1 . z),(F2 . z))
thus F . z = (F1 . z) * (F2 . z) by A3, VALUED_1:5
.= multcomplex . ((F1 . z),(F2 . z)) by BINOP_2:def_5 ; ::_thesis: verum
end;
hence  F = multcomplex .: (F1,F2) by A1, A2, A3, FUNCOP_1:21; ::_thesis: verum
end;
assume A4: F = multcomplex .: (F1,F2) ; ::_thesis: F = mlt (F1,F2)
now__::_thesis:_for_c_being_set_st_c_in_dom_F_holds_
F_._c_=_(F1_._c)_*_(F2_._c)
let c be set ; ::_thesis: ( c in dom F implies F . c = (F1 . c) * (F2 . c) )
assume  c in dom F ; ::_thesis: F . c = (F1 . c) * (F2 . c)
hence F . c = multcomplex . ((F1 . c),(F2 . c)) by A4, FUNCOP_1:22
.= (F1 . c) * (F2 . c) by BINOP_2:def_5 ;
::_thesis: verum
end;
hence  F = mlt (F1,F2) by A1, A4, VALUED_1:def_4; ::_thesis: verum
end;
commutativity
 for b1 being FinSequence of COMPLEX
for F1, F2 being complex-valued FinSequence st b1 = multcomplex .: (F1,F2) holds
b1 = multcomplex .: (F2,F1)
proof
let F be FinSequence of COMPLEX ; ::_thesis: for F1, F2 being complex-valued FinSequence st F = multcomplex .: (F1,F2) holds
F = multcomplex .: (F2,F1)
let F1, F2 be complex-valued FinSequence; ::_thesis: ( F = multcomplex .: (F1,F2) implies F = multcomplex .: (F2,F1) )
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:96;
 [:(rng F3),(rng F4):] c= dom multcomplex by A5, ZFMISC_1:96;
then A7: dom (multcomplex .: (F1,F2)) = (dom F1) /\ (dom F2) by FUNCOP_1:69
.= dom (multcomplex .: (F2,F1)) by A6, FUNCOP_1:69 ;
assume A8: F = multcomplex .: (F1,F2) ; ::_thesis: F = multcomplex .: (F2,F1)
 for z being set st z in dom (multcomplex .: (F2,F1)) holds
F . z = multcomplex . ((F2 . z),(F1 . z))
proof
let z be set ; ::_thesis: ( z in dom (multcomplex .: (F2,F1)) implies F . z = multcomplex . ((F2 . z),(F1 . z)) )
assume A9: z in dom (multcomplex .: (F2,F1)) ; ::_thesis: F . z = multcomplex . ((F2 . z),(F1 . z))
set F1z = F1 . z;
set F2z = F2 . z;
thus F . z = multcomplex . ((F1 . z),(F2 . z)) by A8, A7, A9, FUNCOP_1:22
.= (F1 . z) * (F2 . z) by BINOP_2:def_5
.= multcomplex . ((F2 . z),(F1 . z)) by BINOP_2:def_5 ; ::_thesis: verum
end;
hence  F = multcomplex .: (F2,F1) by A8, A7, FUNCOP_1:21; ::_thesis: verum
end;
end;

:: deftheorem  defines mlt RVSUM_2:def_6_:_
 for F1, F2 being complex-valued FinSequence holds mlt (F1,F2) = multcomplex .: (F1,F2);

definition
let i be Nat;
let R1, R2 be i -element FinSequence of COMPLEX ;
:: original: mlt
redefine func mlt (R1,R2) ->  Element of i -tuples_on COMPLEX;
coherence
 mlt (R1,R2) is Element of i -tuples_on COMPLEX by FINSEQ_2:120;
end;

theorem :: RVSUM_2:25
for F being complex-valued FinSequence holds mlt ((<*> COMPLEX),F) = <*> COMPLEX
proof
let F be complex-valued FinSequence; ::_thesis: mlt ((<*> COMPLEX),F) = <*> COMPLEX
 F is FinSequence of COMPLEX by Lm2;
hence  mlt ((<*> COMPLEX),F) = <*> COMPLEX by FINSEQ_2:73; ::_thesis: verum
end;

theorem :: RVSUM_2:26
for c1, c2 being complex number holds mlt (<*c1*>,<*c2*>) = <*(c1 * c2)*>
proof
let c1, c2 be complex number ; ::_thesis: mlt (<*c1*>,<*c2*>) = <*(c1 * c2)*>
reconsider s1 = c1, s2 = c2 as Element of COMPLEX by XCMPLX_0:def_2;
mlt (<*s1*>,<*s2*>) = <*(multcomplex . (s1,s2))*> by FINSEQ_2:74
.= <*(c1 * c2)*> by BINOP_2:def_5 ;
hence  mlt (<*c1*>,<*c2*>) = <*(c1 * c2)*> ; ::_thesis: verum
end;

theorem Th27: :: RVSUM_2:27
for i being Nat
for c being complex number
for R being b1 -element FinSequence of COMPLEX holds mlt ((i |-> c),R) = c * R
proof
let i be Nat; ::_thesis: for c being complex number
for R being i -element FinSequence of COMPLEX holds mlt ((i |-> c),R) = c * R
let c be complex number ; ::_thesis: for R being i -element FinSequence of COMPLEX holds mlt ((i |-> c),R) = c * R
let R be i -element FinSequence of COMPLEX ; ::_thesis: mlt ((i |-> c),R) = c * R
reconsider s = c as Element of COMPLEX by XCMPLX_0:def_2;
mlt ((i |-> s),R) = multcomplex [;] (s,R) by FINSEQOP:20
.= c * R by FINSEQOP:22 ;
hence  mlt ((i |-> c),R) = c * R ; ::_thesis: verum
end;

theorem :: RVSUM_2:28
for i being Nat
for c1, c2 being complex number holds mlt ((i |-> c1),(i |-> c2)) = i |-> (c1 * c2)
proof
let i be Nat; ::_thesis: for c1, c2 being complex number holds mlt ((i |-> c1),(i |-> c2)) = i |-> (c1 * c2)
let c1, c2 be complex number ; ::_thesis: mlt ((i |-> c1),(i |-> c2)) = i |-> (c1 * c2)
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  mlt ((i |-> c1),(i |-> c2)) = i |-> (c1 * c2) ; ::_thesis: verum
end;

begin

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

theorem :: RVSUM_2:30
for c being complex number holds Sum <*c*> = c
proof
let c be complex number ; ::_thesis: Sum <*c*> = c
reconsider c = c as Element of COMPLEX by XCMPLX_0:def_2;
 Sum <*c*> = c by FINSOP_1:11;
hence  Sum <*c*> = c ; ::_thesis: verum
end;

theorem Th31: :: RVSUM_2:31
for c being complex number
for F being complex-valued FinSequence holds Sum (F ^ <*c*>) = (Sum F) + c
proof
let c be complex number ; ::_thesis: for F being complex-valued FinSequence holds Sum (F ^ <*c*>) = (Sum F) + c
let F be complex-valued FinSequence; ::_thesis: Sum (F ^ <*c*>) = (Sum F) + c
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:4
.= (Sum F1) + c by BINOP_2:def_3
.= (Sum F) + c ; ::_thesis: verum
end;

theorem Th32: :: RVSUM_2:32
for F1, F2 being complex-valued FinSequence holds Sum (F1 ^ F2) = (Sum F1) + (Sum F2)
proof
let F1, F2 be complex-valued FinSequence; ::_thesis: Sum (F1 ^ F2) = (Sum F1) + (Sum F2)
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:5
.= (Sum F3) + (Sum F4) by BINOP_2:def_3
.= (Sum F1) + (Sum F2) ; ::_thesis: verum
end;

theorem :: RVSUM_2:33
for c being complex number
for F being complex-valued FinSequence holds Sum (<*c*> ^ F) = c + (Sum F)
proof
let c be complex number ; ::_thesis: for F being complex-valued FinSequence holds Sum (<*c*> ^ F) = c + (Sum F)
let F be complex-valued FinSequence; ::_thesis: Sum (<*c*> ^ F) = c + (Sum F)
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:11 ; ::_thesis: verum
end;

theorem Th34: :: RVSUM_2:34
for c1, c2 being complex number holds Sum <*c1,c2*> = c1 + c2
proof
let c1, c2 be complex number ; ::_thesis: Sum <*c1,c2*> = c1 + c2
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:11 ; ::_thesis: verum
end;

theorem :: RVSUM_2:35
for c1, c2, c3 being complex number holds Sum <*c1,c2,c3*> = (c1 + c2) + c3
proof
let c1, c2, c3 be complex number ; ::_thesis: Sum <*c1,c2,c3*> = (c1 + c2) + c3
thus  Sum <*c1,c2,c3*> = (Sum <*c1,c2*>) + c3 by Th31
.= (c1 + c2) + c3 by Th34 ; ::_thesis: verum
end;

theorem Th36: :: RVSUM_2:36
for i being Nat
for c being complex number holds Sum (i |-> c) = i * c
proof
let i be Nat; ::_thesis: for c being complex number holds Sum (i |-> c) = i * c
let c be complex number ; ::_thesis: Sum (i |-> c) = i * c
reconsider c = c as Element of COMPLEX by XCMPLX_0:def_2;
defpred S1[ Nat] means  Sum ($1 |-> c) = $1 * c;
A1: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A2: Sum (i |-> c) = i * c ; ::_thesis: S1[i + 1]
thus  Sum ((i + 1) |-> c) = Sum ((i |-> c) ^ <*c*>) by FINSEQ_2:60
.= (i * c) + (1 * c) by A2, Th31
.= (i + 1) * c ; ::_thesis: verum
end;
A3: S1[ 0 ] by Th29;
 for i being Nat holds S1[i] from NAT_1:sch_2(A3, A1);
hence  Sum (i |-> c) = i * c ; ::_thesis: verum
end;

theorem :: RVSUM_2:37
for i being Nat holds Sum (i |-> 0c) = 0c
proof
let i be Nat; ::_thesis: Sum (i |-> 0c) = 0c
thus  Sum (i |-> 0c) = i * 0 by Th36
.= 0c ; ::_thesis: verum
end;

theorem :: RVSUM_2:38
for c being complex number
for F being complex-valued FinSequence holds Sum (c * F) = c * (Sum F)
proof
let c be complex number ; ::_thesis: for F being complex-valued FinSequence holds Sum (c * F) = c * (Sum F)
let F be complex-valued FinSequence; ::_thesis: Sum (c * F) = c * (Sum F)
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) = (multcomplex [;] (s,(id COMPLEX))) . (addcomplex $$ F1) by SEQ_4:51, SEQ_4:54, SETWOP_2:30
.= c * (Sum F1) by Lm1
.= c * (Sum F) ; ::_thesis: verum
end;

theorem Th39: :: RVSUM_2:39
for F being complex-valued FinSequence holds Sum (- F) = - (Sum F)
proof
let F be complex-valued FinSequence; ::_thesis: Sum (- F) = - (Sum F)
reconsider F1 = F as FinSequence of COMPLEX by Lm2;
thus  Sum (- F) = compcomplex . (addcomplex $$ F1) by SEQ_4:51, SEQ_4:52, SETWOP_2:31
.= - (Sum F1) by BINOP_2:def_1
.= - (Sum F) ; ::_thesis: verum
end;

theorem Th40: :: RVSUM_2:40
for i being Nat
for R1, R2 being b1 -element FinSequence of COMPLEX holds Sum (R1 + R2) = (Sum R1) + (Sum R2)
proof
let i be Nat; ::_thesis: for R1, R2 being i -element FinSequence of COMPLEX holds Sum (R1 + R2) = (Sum R1) + (Sum R2)
let R1, R2 be i -element FinSequence of COMPLEX ; ::_thesis: Sum (R1 + R2) = (Sum R1) + (Sum R2)
reconsider T1 = R1, T2 = R2 as Element of i -tuples_on COMPLEX by FINSEQ_2:131;
thus  Sum (R1 + R2) = addcomplex . ((addcomplex $$ T1),(addcomplex $$ T2)) by SETWOP_2:35
.= (Sum R1) + (Sum R2) by BINOP_2:def_3 ; ::_thesis: verum
end;

theorem :: RVSUM_2:41
for i being Nat
for R1, R2 being b1 -element FinSequence of COMPLEX holds Sum (R1 - R2) = (Sum R1) - (Sum R2)
proof
let i be Nat; ::_thesis: for R1, R2 being i -element FinSequence of COMPLEX holds Sum (R1 - R2) = (Sum R1) - (Sum R2)
let R1, R2 be i -element FinSequence of COMPLEX ; ::_thesis: Sum (R1 - R2) = (Sum R1) - (Sum R2)
thus  Sum (R1 - R2) = (Sum R1) + (Sum (- R2)) by Th40
.= (Sum R1) - (Sum R2) by Th39 ; ::_thesis: verum
end;

begin

Lm3:  for F being empty FinSequence holds Product F = 1
proof
 Product (<*> COMPLEX) = 1 by BINOP_2:6, FINSOP_1:10;
hence  for F being empty FinSequence holds Product F = 1 ; ::_thesis: verum
end;

theorem :: RVSUM_2:42
Product (<*> COMPLEX) = 1 by Lm3;

theorem :: RVSUM_2:43
for c being complex number
for F being complex-valued FinSequence holds Product (<*c*> ^ F) = c * (Product F)
proof
let c be complex number ; ::_thesis: for F being complex-valued FinSequence holds Product (<*c*> ^ F) = c * (Product F)
let F be complex-valued FinSequence; ::_thesis: Product (<*c*> ^ F) = c * (Product F)
thus  Product (<*c*> ^ F) = (Product <*c*>) * (Product F) by RVSUM_1:97
.= c * (Product F) by RVSUM_1:95 ; ::_thesis: verum
end;

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

theorem :: RVSUM_2:45
for i, j being Nat
for c being complex number holds Product ((i + j) |-> c) = (Product (i |-> c)) * (Product (j |-> c))
proof
let i, j be Nat; ::_thesis: for c being complex number holds Product ((i + j) |-> c) = (Product (i |-> c)) * (Product (j |-> c))
let c be complex number ; ::_thesis: Product ((i + j) |-> c) = (Product (i |-> c)) * (Product (j |-> c))
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:26
.= (Product (i |-> s)) * (Product (j |-> s)) by BINOP_2:def_5 ;
hence  Product ((i + j) |-> c) = (Product (i |-> c)) * (Product (j |-> c)) ; ::_thesis: verum
end;

theorem :: RVSUM_2:46
for i, j being Nat
for c being complex number holds Product ((i * j) |-> c) = Product (j |-> (Product (i |-> c)))
proof
let i, j be Nat; ::_thesis: for c being complex number holds Product ((i * j) |-> c) = Product (j |-> (Product (i |-> c)))
let c be complex number ; ::_thesis: Product ((i * j) |-> c) = Product (j |-> (Product (i |-> c)))
reconsider c = c as Element of COMPLEX by XCMPLX_0:def_2;
 Product ((i * j) |-> c) = Product (j |-> (Product (i |-> c))) by SETWOP_2:27;
hence  Product ((i * j) |-> c) = Product (j |-> (Product (i |-> c))) ; ::_thesis: verum
end;

theorem :: RVSUM_2:47
for i being Nat
for c1, c2 being complex number holds Product (i |-> (c1 * c2)) = (Product (i |-> c1)) * (Product (i |-> c2))
proof
let i be Nat; ::_thesis: for c1, c2 being complex number holds Product (i |-> (c1 * c2)) = (Product (i |-> c1)) * (Product (i |-> c2))
let c1, c2 be complex number ; ::_thesis: Product (i |-> (c1 * c2)) = (Product (i |-> c1)) * (Product (i |-> c2))
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:36
.= (Product (i |-> s1)) * (Product (i |-> s2)) by BINOP_2:def_5 ;
hence  Product (i |-> (c1 * c2)) = (Product (i |-> c1)) * (Product (i |-> c2)) ; ::_thesis: verum
end;

theorem Th48: :: RVSUM_2:48
for i being Nat
for R1, R2 being b1 -element FinSequence of COMPLEX holds Product (mlt (R1,R2)) = (Product R1) * (Product R2)
proof
let i be Nat; ::_thesis: for R1, R2 being i -element FinSequence of COMPLEX holds Product (mlt (R1,R2)) = (Product R1) * (Product R2)
let R1, R2 be i -element FinSequence of COMPLEX ; ::_thesis: Product (mlt (R1,R2)) = (Product R1) * (Product R2)
reconsider T1 = R1, T2 = R2 as Element of i -tuples_on COMPLEX by FINSEQ_2:131;
thus  Product (mlt (R1,R2)) = multcomplex . ((multcomplex $$ T1),(multcomplex $$ T2)) by SETWOP_2:35
.= (Product R1) * (Product R2) by BINOP_2:def_5 ; ::_thesis: verum
end;

theorem :: RVSUM_2:49
for i being Nat
for c being complex number
for R being b1 -element FinSequence of COMPLEX holds Product (c * R) = (Product (i |-> c)) * (Product R)
proof
let i be Nat; ::_thesis: for c being complex number
for R being i -element FinSequence of COMPLEX holds Product (c * R) = (Product (i |-> c)) * (Product R)
let c be complex number ; ::_thesis: for R being i -element FinSequence of COMPLEX holds Product (c * R) = (Product (i |-> c)) * (Product R)
let R be i -element FinSequence of COMPLEX ; ::_thesis: Product (c * R) = (Product (i |-> c)) * (Product R)
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 ; ::_thesis: verum
end;

begin

theorem :: RVSUM_2:50
for x being complex-valued FinSequence holds len (- x) = len x
proof
let x be complex-valued FinSequence; ::_thesis: len (- x) = len x
 dom (- x) = dom x by VALUED_1:8;
hence  len (- x) = len x by FINSEQ_3:29; ::_thesis: verum
end;

theorem :: RVSUM_2:51
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; ::_thesis: ( len x1 = len x2 implies len (x1 + x2) = len x1 )
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:92;
assume  len x1 = len x2 ; ::_thesis: len (x1 + x2) = len x1
then reconsider z2 = x2 as Element of (len x1) -tuples_on COMPLEX by A1, FINSEQ_2:92;
 dom (z1 + z2) = Seg (len x1) by FINSEQ_2:124;
hence  len (x1 + x2) = len x1 by FINSEQ_1:def_3; ::_thesis: verum
end;

theorem :: RVSUM_2:52
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; ::_thesis: ( len x1 = len x2 implies len (x1 - x2) = len x1 )
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:92;
assume  len x1 = len x2 ; ::_thesis: len (x1 - x2) = len x1
then reconsider z2 = x2 as Element of (len x1) -tuples_on COMPLEX by A1, FINSEQ_2:92;
 dom (z1 - z2) = Seg (len x1) by FINSEQ_2:124;
hence  len (x1 - x2) = len x1 by FINSEQ_1:def_3; ::_thesis: verum
end;

theorem :: RVSUM_2:53
for a being real number
for x being complex-valued FinSequence holds len (a * x) = len x
proof
let a be real number ; ::_thesis: for x being complex-valued FinSequence holds len (a * x) = len x
let x be complex-valued FinSequence; ::_thesis: len (a * x) = len x
set n = len x;
 x is FinSequence of COMPLEX by Lm2;
then reconsider z = x as Element of (len x) -tuples_on COMPLEX by FINSEQ_2:92;
 len (a * z) = len x by CARD_1:def_7;
hence  len (a * x) = len x ; ::_thesis: verum
end;

theorem :: RVSUM_2:54
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; ::_thesis: ( len x = len y & len y = len z implies mlt ((x + y),z) = (mlt (x,z)) + (mlt (y,z)) )
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 ) ; ::_thesis: mlt ((x + y),z) = (mlt (x,z)) + (mlt (y,z))
then reconsider x2 = x, y2 = y, z2 = z as Element of (len x) -tuples_on COMPLEX by A1, FINSEQ_2:92;
A2: dom (mlt ((x + y),z)) = Seg (len (mlt ((x2 + y2),z2))) by FINSEQ_1:def_3
.= Seg (len x) by CARD_1:def_7
.= Seg (len ((mlt (x2,z2)) + (mlt (y2,z2)))) by CARD_1:def_7
.= 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 CARD_1:def_7
.= Seg (len ((mlt (x2,z2)) + (mlt (y2,z2)))) by CARD_1:def_7
.= 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; ::_thesis: ( i in dom (mlt ((x + y),z)) implies (mlt ((x + y),z)) . i = ((mlt (x,z)) + (mlt (y,z))) . i )
assume A4: i in dom (mlt ((x + y),z)) ; ::_thesis: (mlt ((x + y),z)) . i = ((mlt (x,z)) + (mlt (y,z))) . i
set a = x . i;
set b = y . i;
set d = (x + y) . i;
set e = z . i;
 len (x2 + y2) = len x by CARD_1:def_7;
then  dom (x2 + y2) = Seg (len x) by FINSEQ_1:def_3
.= Seg (len (mlt (x2,z2))) by CARD_1:def_7
.= dom (mlt (x,z)) by FINSEQ_1:def_3 ;
then A5: (x + y) . i = (x . i) + (y . i) by A2, A3, A4, VALUED_1:def_1;
thus (mlt ((x + y),z)) . i = ((x + y) . i) * (z . i) by VALUED_1:5
.= ((x . i) * (z . i)) + ((y . i) * (z . i)) by A5
.= ((mlt (x,z)) . i) + ((y . i) * (z . i)) 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 ; ::_thesis: verum
end;
hence  mlt ((x + y),z) = (mlt (x,z)) + (mlt (y,z)) by A2, FINSEQ_1:13; ::_thesis: verum
end;