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_3)) * (P . ((E /. i) `2_3))) * (P . ((E /. i) `3_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_3)) * (P . ((E /. i) `2_3))) * (P . ((E /. i) `3_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_3)) * (P . ((E /. i) `2_3))) * (P . ((E /. i) `3_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_3)) * (P . ((E /. i) `2_3))) * (P . ((E /. i) `3_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_3)) * (P . ((E /. i) `2_3))) * (P . ((E /. i) `3_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_3)) * (P . ((E /. i) `2_3))) * (P . ((E /. i) `3_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_3)) * (P . ((E /. i) `2_3))) * (P . ((E /. i) `3_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_3)) * (P . ((E /. i) `2_3))) * (P . ((E /. i) `3_3)) ; :: thesis: P . (Sum lc) = Sum LC
defpred S₁[ Nat] means for lc9 being LinearCombination of F
for LC9 being LinearCombination of G st lc9 = lc | (Seg $1) & LC9 = LC | (Seg $1) holds
P . (Sum lc9) = Sum LC9;
A5: ( P is additive & P is multiplicative ) by A1;
A6: dom lc = dom LC by A2, FINSEQ_3:29;
A7: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A8: S₁[k] ; :: thesis: S₁[k + 1]
thus S₁[k + 1] :: thesis: verum

proof

let lc9 be LinearCombination of F; :: thesis: for LC9 being LinearCombination of G st lc9 = lc | (Seg (k + 1)) & LC9 = LC | (Seg (k + 1)) holds
P . (Sum lc9) = Sum LC9
let LC9 be LinearCombination of G; :: thesis: ( lc9 = lc | (Seg (k + 1)) & LC9 = LC | (Seg (k + 1)) implies P . (Sum lc9) = Sum LC9 )
assume that
A9: lc9 = lc | (Seg (k + 1)) and
A10: LC9 = LC | (Seg (k + 1)) ; :: thesis: P . (Sum lc9) = Sum LC9

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

suppose A11: len lc < k + 1 ; :: thesis: P . (Sum lc9) = Sum LC9

then A12: len lc <= k by NAT_1:13;
A13: lc9 = lc by A9, A11, FINSEQ_3:49
.= lc | (Seg k) by A12, FINSEQ_3:49 ;
LC9 = LC by A2, A10, A11, FINSEQ_3:49
.= LC | (Seg k) by A2, A12, FINSEQ_3:49 ;
hence P . (Sum lc9) = Sum LC9 by A8, A13; :: thesis: verum

end;

suppose A14: len lc >= k + 1 ; :: thesis: P . (Sum lc9) = Sum LC9

set i = k + 1;
reconsider LCk = LC | (Seg k) as LinearCombination of G by IDEAL_1:41;
reconsider lck = lc | (Seg k) as LinearCombination of F by IDEAL_1:41;
1 <= k + 1 by NAT_1:11;
then A15: k + 1 in dom lc by A14, FINSEQ_3:25;
then A16: lc . (k + 1) = lc /. (k + 1) by PARTFUN1:def 6;
A17: LC . (k + 1) = LC /. (k + 1) by A6, A15, PARTFUN1:def 6;
lc | (Seg (k + 1)) = lck ^ <*(lc . (k + 1))*> by A15, FINSEQ_5:10;
hence P . (Sum lc9) = P . ((Sum lck) + (lc /. (k + 1))) by A9, A16, FVSUM_1:71
.= (P . (Sum lck)) + (P . (lc /. (k + 1))) by A5
.= (Sum LCk) + (P . (lc /. (k + 1))) by A8
.= (Sum LCk) + (P . ((((E /. (k + 1)) `1_3) * ((E /. (k + 1)) `2_3)) * ((E /. (k + 1)) `3_3))) by A3, A15, A16
.= (Sum LCk) + ((P . (((E /. (k + 1)) `1_3) * ((E /. (k + 1)) `2_3))) * (P . ((E /. (k + 1)) `3_3))) by A5
.= (Sum LCk) + (((P . ((E /. (k + 1)) `1_3)) * (P . ((E /. (k + 1)) `2_3))) * (P . ((E /. (k + 1)) `3_3))) by A5
.= (Sum LCk) + (LC /. (k + 1)) by A4, A6, A15, A17
.= Sum (LCk ^ <*(LC /. (k + 1))*>) by FVSUM_1:71
.= Sum LC9 by A6, A10, A15, A17, FINSEQ_5:10 ;
:: thesis: verum

end;

end;

end;

end;

A18: ( lc = lc | (Seg (len lc)) & LC = LC | (Seg (len LC)) ) by FINSEQ_3:49;
A19: S₁[ 0 ]

proof

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

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A19, A7);
hence P . (Sum lc) = Sum LC by A2, A18; :: thesis: verum