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 S1[ 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 ;
A7: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A8: S1[k] ; :: thesis: S1[k + 1]
thus S1[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
.= lc | (Seg k) by ;
LC9 = LC by
.= LC | (Seg k) by ;
hence P . (Sum lc9) = Sum LC9 by ; :: 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 ;
then A16: lc . (k + 1) = lc /. (k + 1) by PARTFUN1:def 6;
A17: LC . (k + 1) = LC /. (k + 1) by ;
lc | (Seg (k + 1)) = lck ^ <*(lc . (k + 1))*> by ;
hence P . (Sum lc9) = P . ((Sum lck) + (lc /. (k + 1))) by
.= (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 ;
:: thesis: verum
end;
end;
end;
end;
A18: ( lc = lc | (Seg (len lc)) & LC = LC | (Seg (len LC)) ) by FINSEQ_3:49;
A19: S1[ 0 ]
proof
let lc9 be LinearCombination of F; :: thesis: for LC9 being LinearCombination of G st lc9 = lc | () & LC9 = LC | () holds
P . (Sum lc9) = Sum LC9

let LC9 be LinearCombination of G; :: thesis: ( lc9 = lc | () & LC9 = LC | () implies P . (Sum lc9) = Sum LC9 )
assume that
A20: lc9 = lc | () and
A21: LC9 = LC | () ; :: 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
.= Sum (<*> the carrier of S) by RLVECT_1:43
.= Sum LC9 by A21 ; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A19, A7);
hence P . (Sum lc) = Sum LC by ; :: thesis: verum