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_{1}[ 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_{1}[k] holds

S_{1}[k + 1]

A19: S_{1}[ 0 ]
_{1}[k]
from NAT_1:sch 2(A19, A7);

hence P . (Sum lc) = Sum LC by A2, A18; :: thesis: verum

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

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

S

proof

A18:
( lc = lc | (Seg (len lc)) & LC = LC | (Seg (len LC)) )
by FINSEQ_3:49;
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A8: S_{1}[k]
; :: thesis: S_{1}[k + 1]

thus S_{1}[k + 1]
:: thesis: verum

end;assume A8: S

thus S

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

end;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 )
;

end;

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;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

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;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

A19: S

proof

for k being Nat holds S
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;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

hence P . (Sum lc) = Sum LC by A2, A18; :: thesis: verum