let R, S be non empty right_complementable add-associative right_zeroed doubleLoopStr ; :: thesis: for F being non empty Subset of R
for G being non empty Subset of S
for P being Function of R,S
for lc being LinearCombination of F
for LC being LinearCombination of G
for E being FinSequence of [:the carrier of R,the carrier of R,the carrier of R:] st P is RingHomomorphism & len lc = len LC & E represents lc & ( for i being set st i in dom LC holds
LC . i = ((P . ((E /. i) `1 )) * (P . ((E /. i) `2 ))) * (P . ((E /. i) `3 )) ) holds
P . (Sum lc) = Sum LC
let F be non empty Subset of R; :: thesis: for G being non empty Subset of S
for P being Function of R,S
for lc being LinearCombination of F
for LC being LinearCombination of G
for E being FinSequence of [:the carrier of R,the carrier of R,the carrier of R:] st P is RingHomomorphism & len lc = len LC & E represents lc & ( for i being set st i in dom LC holds
LC . i = ((P . ((E /. i) `1 )) * (P . ((E /. i) `2 ))) * (P . ((E /. i) `3 )) ) holds
P . (Sum lc) = Sum LC
let G be non empty Subset of S; :: thesis: for P being Function of R,S
for lc being LinearCombination of F
for LC being LinearCombination of G
for E being FinSequence of [:the carrier of R,the carrier of R,the carrier of R:] st P is RingHomomorphism & len lc = len LC & E represents lc & ( for i being set st i in dom LC holds
LC . i = ((P . ((E /. i) `1 )) * (P . ((E /. i) `2 ))) * (P . ((E /. i) `3 )) ) holds
P . (Sum lc) = Sum LC
let P be Function of R,S; :: thesis: for lc being LinearCombination of F
for LC being LinearCombination of G
for E being FinSequence of [:the carrier of R,the carrier of R,the carrier of R:] st P is RingHomomorphism & len lc = len LC & E represents lc & ( for i being set st i in dom LC holds
LC . i = ((P . ((E /. i) `1 )) * (P . ((E /. i) `2 ))) * (P . ((E /. i) `3 )) ) holds
P . (Sum lc) = Sum LC
let lc be LinearCombination of F; :: thesis: for LC being LinearCombination of G
for E being FinSequence of [:the carrier of R,the carrier of R,the carrier of R:] st P is RingHomomorphism & len lc = len LC & E represents lc & ( for i being set st i in dom LC holds
LC . i = ((P . ((E /. i) `1 )) * (P . ((E /. i) `2 ))) * (P . ((E /. i) `3 )) ) holds
P . (Sum lc) = Sum LC
let LC be LinearCombination of G; :: thesis: for E being FinSequence of [:the carrier of R,the carrier of R,the carrier of R:] st P is RingHomomorphism & len lc = len LC & E represents lc & ( for i being set st i in dom LC holds
LC . i = ((P . ((E /. i) `1 )) * (P . ((E /. i) `2 ))) * (P . ((E /. i) `3 )) ) holds
P . (Sum lc) = Sum LC
let E be FinSequence of [:the carrier of R,the carrier of R,the carrier of R:]; :: thesis: ( P is RingHomomorphism & len lc = len LC & E represents lc & ( for i being set st i in dom LC holds
LC . i = ((P . ((E /. i) `1 )) * (P . ((E /. i) `2 ))) * (P . ((E /. i) `3 )) ) implies P . (Sum lc) = Sum LC )
assume that
A1: P is RingHomomorphism and
A2: len lc = len LC and
A3: E represents lc and
A4: for i being set st i in dom LC holds
LC . i = ((P . ((E /. i) `1 )) * (P . ((E /. i) `2 ))) * (P . ((E /. i) `3 )) ; :: thesis: P . (Sum lc) = Sum LC
A5: dom lc = dom LC by A2, FINSEQ_3:31;
A6: ( P is additive & P is multiplicative ) by A1, QUOFIELD:def 21;
defpred S₁[ Element of NAT ] means for lc' being LinearCombination of F
for LC' being LinearCombination of G st lc' = lc | (Seg $1) & LC' = LC | (Seg $1) holds
P . (Sum lc') = Sum LC';
A7: S₁[ 0 ]

proof

let lc' be LinearCombination of F; :: thesis: for LC' being LinearCombination of G st lc' = lc | (Seg 0 ) & LC' = LC | (Seg 0 ) holds
P . (Sum lc') = Sum LC'
let LC' be LinearCombination of G; :: thesis: ( lc' = lc | (Seg 0 ) & LC' = LC | (Seg 0 ) implies P . (Sum lc') = Sum LC' )
assume A8: ( lc' = lc | (Seg 0 ) & LC' = LC | (Seg 0 ) ) ; :: thesis: P . (Sum lc') = Sum LC'
thus P . (Sum lc') = P . (Sum (<*> the carrier of R)) by A8
.= P . (0. R) by RLVECT_1:60
.= 0. S by A1, Th23
.= Sum (<*> the carrier of S) by RLVECT_1:60
.= Sum LC' by A8 ; :: thesis: verum

end;

A9: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A10: S₁[k] ; :: thesis: S₁[k + 1]
thus S₁[k + 1] :: thesis: verum

proof

let lc' be LinearCombination of F; :: thesis: for LC' being LinearCombination of G st lc' = lc | (Seg (k + 1)) & LC' = LC | (Seg (k + 1)) holds
P . (Sum lc') = Sum LC'
let LC' be LinearCombination of G; :: thesis: ( lc' = lc | (Seg (k + 1)) & LC' = LC | (Seg (k + 1)) implies P . (Sum lc') = Sum LC' )
assume A11: ( lc' = lc | (Seg (k + 1)) & LC' = LC | (Seg (k + 1)) ) ; :: thesis: P . (Sum lc') = Sum LC'

per cases ( len lc < k + 1 or len lc >= k + 1 ) ;

suppose A12: len lc < k + 1 ; :: thesis: P . (Sum lc') = Sum LC'

then A13: len lc <= k by NAT_1:13;
A14: lc' = lc by A11, A12, FINSEQ_3:55
.= lc | (Seg k) by A13, FINSEQ_3:55 ;
LC' = LC by A2, A11, A12, FINSEQ_3:55
.= LC | (Seg k) by A2, A13, FINSEQ_3:55 ;
hence P . (Sum lc') = Sum LC' by A10, A14; :: thesis: verum

end;

suppose A15: len lc >= k + 1 ; :: thesis: P . (Sum lc') = Sum LC'

1 <= k + 1 by NAT_1:11;
then A16: k + 1 in dom lc by A15, FINSEQ_3:27;
reconsider lck = lc | (Seg k) as LinearCombination of F by IDEAL_1:41;
reconsider LCk = LC | (Seg k) as LinearCombination of G by IDEAL_1:41;
set i = k + 1;
A17: lc | (Seg (k + 1)) = lck ^ <*(lc . (k + 1))*> by A16, FINSEQ_5:11;
A18: LC . (k + 1) = LC /. (k + 1) by A5, A16, PARTFUN1:def 8;
A19: lc . (k + 1) = lc /. (k + 1) by A16, PARTFUN1:def 8;
hence P . (Sum lc') = P . ((Sum lck) + (lc /. (k + 1))) by A11, A17, FVSUM_1:87
.= (P . (Sum lck)) + (P . (lc /. (k + 1))) by A6, GRCAT_1:def 13
.= (Sum LCk) + (P . (lc /. (k + 1))) by A10
.= (Sum LCk) + (P . ((((E /. (k + 1)) `1 ) * ((E /. (k + 1)) `2 )) * ((E /. (k + 1)) `3 ))) by A3, A16, A19, IDEAL_1:def 12
.= (Sum LCk) + ((P . (((E /. (k + 1)) `1 ) * ((E /. (k + 1)) `2 ))) * (P . ((E /. (k + 1)) `3 ))) by A6, GROUP_6:def 7
.= (Sum LCk) + (((P . ((E /. (k + 1)) `1 )) * (P . ((E /. (k + 1)) `2 ))) * (P . ((E /. (k + 1)) `3 ))) by A6, GROUP_6:def 7
.= (Sum LCk) + (LC /. (k + 1)) by A4, A5, A16, A18
.= Sum (LCk ^ <*(LC /. (k + 1))*>) by FVSUM_1:87
.= Sum LC' by A5, A11, A16, A18, FINSEQ_5:11 ;
:: thesis: verum

end;

end;

end;

end;

A20: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A7, A9);
( lc = lc | (Seg (len lc)) & LC = LC | (Seg (len LC)) ) by FINSEQ_3:55;
hence P . (Sum lc) = Sum LC by A2, A20; :: thesis: verum