let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for F, G, H being FinSequence of the carrier of V st len F = len G & len F = len H & ( for k being Nat st k in dom F holds

H . k = (F /. k) + (G /. k) ) holds

Sum H = (Sum F) + (Sum G)

defpred S_{1}[ Nat] means for F, G, H being FinSequence of the carrier of V st len F = $1 & len F = len G & len F = len H & ( for k being Nat st k in dom F holds

H . k = (F /. k) + (G /. k) ) holds

Sum H = (Sum F) + (Sum G);

_{1}[k] holds

S_{1}[k + 1]
;

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

hence for F, G, H being FinSequence of the carrier of V st len F = len G & len F = len H & ( for k being Nat st k in dom F holds

H . k = (F /. k) + (G /. k) ) holds

Sum H = (Sum F) + (Sum G) ; :: thesis: verum

H . k = (F /. k) + (G /. k) ) holds

Sum H = (Sum F) + (Sum G)

defpred S

H . k = (F /. k) + (G /. k) ) holds

Sum H = (Sum F) + (Sum G);

now :: thesis: for k being Nat st ( for F, G, H being FinSequence of the carrier of V st len F = k & len F = len G & len F = len H & ( for k being Nat st k in dom F holds

H . k = (F /. k) + (G /. k) ) holds

Sum H = (Sum F) + (Sum G) ) holds

for F, G, H being FinSequence of the carrier of V st len F = k + 1 & len F = len G & len F = len H & ( for k being Nat st k in dom F holds

H . k = (F /. k) + (G /. k) ) holds

Sum H = (Sum F) + (Sum G)

then A27:
for k being Nat st SH . k = (F /. k) + (G /. k) ) holds

Sum H = (Sum F) + (Sum G) ) holds

for F, G, H being FinSequence of the carrier of V st len F = k + 1 & len F = len G & len F = len H & ( for k being Nat st k in dom F holds

H . k = (F /. k) + (G /. k) ) holds

Sum H = (Sum F) + (Sum G)

let k be Nat; :: thesis: ( ( for F, G, H being FinSequence of the carrier of V st len F = k & len F = len G & len F = len H & ( for k being Nat st k in dom F holds

H . k = (F /. k) + (G /. k) ) holds

Sum H = (Sum F) + (Sum G) ) implies for F, G, H being FinSequence of the carrier of V st len F = k + 1 & len F = len G & len F = len H & ( for k being Nat st k in dom F holds

H . k = (F /. k) + (G /. k) ) holds

Sum H = (Sum F) + (Sum G) )

assume A1: for F, G, H being FinSequence of the carrier of V st len F = k & len F = len G & len F = len H & ( for k being Nat st k in dom F holds

H . k = (F /. k) + (G /. k) ) holds

Sum H = (Sum F) + (Sum G) ; :: thesis: for F, G, H being FinSequence of the carrier of V st len F = k + 1 & len F = len G & len F = len H & ( for k being Nat st k in dom F holds

H . k = (F /. k) + (G /. k) ) holds

Sum H = (Sum F) + (Sum G)

let F, G, H be FinSequence of the carrier of V; :: thesis: ( len F = k + 1 & len F = len G & len F = len H & ( for k being Nat st k in dom F holds

H . k = (F /. k) + (G /. k) ) implies Sum H = (Sum F) + (Sum G) )

assume that

A2: len F = k + 1 and

A3: len F = len G and

A4: len F = len H and

A5: for k being Nat st k in dom F holds

H . k = (F /. k) + (G /. k) ; :: thesis: Sum H = (Sum F) + (Sum G)

reconsider f = F | (Seg k), g = G | (Seg k), h = H | (Seg k) as FinSequence of the carrier of V by FINSEQ_1:18;

A6: len h = k by A2, A4, FINSEQ_3:53;

A7: k + 1 in Seg (k + 1) by FINSEQ_1:4;

then A8: k + 1 in dom G by A2, A3, FINSEQ_1:def 3;

then A9: G . (k + 1) in rng G by FUNCT_1:def 3;

k + 1 in dom H by A2, A4, A7, FINSEQ_1:def 3;

then A10: H . (k + 1) in rng H by FUNCT_1:def 3;

A11: k + 1 in dom F by A2, A7, FINSEQ_1:def 3;

then F . (k + 1) in rng F by FUNCT_1:def 3;

then reconsider v = F . (k + 1), u = G . (k + 1), w = H . (k + 1) as Element of V by A9, A10;

A12: w = (F /. (k + 1)) + (G /. (k + 1)) by A5, A11

.= v + (G /. (k + 1)) by A11, PARTFUN1:def 6

.= v + u by A8, PARTFUN1:def 6 ;

G = g ^ <*u*> by A2, A3, FINSEQ_3:55;

then A13: Sum G = (Sum g) + (Sum <*u*>) by RLVECT_1:41;

A14: Sum <*v*> = v by RLVECT_1:44;

A15: len f = k by A2, FINSEQ_3:53;

A16: len g = k by A2, A3, FINSEQ_3:53;

F = f ^ <*v*> by A2, FINSEQ_3:55;

then A25: Sum F = (Sum f) + (Sum <*v*>) by RLVECT_1:41;

A26: Sum <*u*> = u by RLVECT_1:44;

H = h ^ <*w*> by A2, A4, FINSEQ_3:55;

hence Sum H = (Sum h) + (Sum <*w*>) by RLVECT_1:41

.= ((Sum f) + (Sum g)) + (v + u) by A24, A12, RLVECT_1:44

.= (((Sum f) + (Sum g)) + v) + u by RLVECT_1:def 3

.= ((Sum F) + (Sum g)) + u by A25, A14, RLVECT_1:def 3

.= (Sum F) + (Sum G) by A13, A26, RLVECT_1:def 3 ;

:: thesis: verum

end;H . k = (F /. k) + (G /. k) ) holds

Sum H = (Sum F) + (Sum G) ) implies for F, G, H being FinSequence of the carrier of V st len F = k + 1 & len F = len G & len F = len H & ( for k being Nat st k in dom F holds

H . k = (F /. k) + (G /. k) ) holds

Sum H = (Sum F) + (Sum G) )

assume A1: for F, G, H being FinSequence of the carrier of V st len F = k & len F = len G & len F = len H & ( for k being Nat st k in dom F holds

H . k = (F /. k) + (G /. k) ) holds

Sum H = (Sum F) + (Sum G) ; :: thesis: for F, G, H being FinSequence of the carrier of V st len F = k + 1 & len F = len G & len F = len H & ( for k being Nat st k in dom F holds

H . k = (F /. k) + (G /. k) ) holds

Sum H = (Sum F) + (Sum G)

let F, G, H be FinSequence of the carrier of V; :: thesis: ( len F = k + 1 & len F = len G & len F = len H & ( for k being Nat st k in dom F holds

H . k = (F /. k) + (G /. k) ) implies Sum H = (Sum F) + (Sum G) )

assume that

A2: len F = k + 1 and

A3: len F = len G and

A4: len F = len H and

A5: for k being Nat st k in dom F holds

H . k = (F /. k) + (G /. k) ; :: thesis: Sum H = (Sum F) + (Sum G)

reconsider f = F | (Seg k), g = G | (Seg k), h = H | (Seg k) as FinSequence of the carrier of V by FINSEQ_1:18;

A6: len h = k by A2, A4, FINSEQ_3:53;

A7: k + 1 in Seg (k + 1) by FINSEQ_1:4;

then A8: k + 1 in dom G by A2, A3, FINSEQ_1:def 3;

then A9: G . (k + 1) in rng G by FUNCT_1:def 3;

k + 1 in dom H by A2, A4, A7, FINSEQ_1:def 3;

then A10: H . (k + 1) in rng H by FUNCT_1:def 3;

A11: k + 1 in dom F by A2, A7, FINSEQ_1:def 3;

then F . (k + 1) in rng F by FUNCT_1:def 3;

then reconsider v = F . (k + 1), u = G . (k + 1), w = H . (k + 1) as Element of V by A9, A10;

A12: w = (F /. (k + 1)) + (G /. (k + 1)) by A5, A11

.= v + (G /. (k + 1)) by A11, PARTFUN1:def 6

.= v + u by A8, PARTFUN1:def 6 ;

G = g ^ <*u*> by A2, A3, FINSEQ_3:55;

then A13: Sum G = (Sum g) + (Sum <*u*>) by RLVECT_1:41;

A14: Sum <*v*> = v by RLVECT_1:44;

A15: len f = k by A2, FINSEQ_3:53;

A16: len g = k by A2, A3, FINSEQ_3:53;

now :: thesis: for i being Nat st i in dom f holds

h . i = (f /. i) + (g /. i)

then A24:
Sum h = (Sum f) + (Sum g)
by A1, A15, A16, A6;h . i = (f /. i) + (g /. i)

let i be Nat; :: thesis: ( i in dom f implies h . i = (f /. i) + (g /. i) )

assume A17: i in dom f ; :: thesis: h . i = (f /. i) + (g /. i)

then A18: F . i = f . i by FUNCT_1:47;

len f <= len F by A2, A15, NAT_1:12;

then A19: dom f c= dom F by FINSEQ_3:30;

then i in dom F by A17;

then i in dom G by A3, FINSEQ_3:29;

then A20: G /. i = G . i by PARTFUN1:def 6;

i in dom h by A15, A6, A17, FINSEQ_3:29;

then A21: H . i = h . i by FUNCT_1:47;

F /. i = F . i by A17, A19, PARTFUN1:def 6;

then A22: f /. i = F /. i by A17, A18, PARTFUN1:def 6;

A23: i in dom g by A15, A16, A17, FINSEQ_3:29;

then G . i = g . i by FUNCT_1:47;

then g /. i = G /. i by A23, A20, PARTFUN1:def 6;

hence h . i = (f /. i) + (g /. i) by A5, A17, A21, A19, A22; :: thesis: verum

end;assume A17: i in dom f ; :: thesis: h . i = (f /. i) + (g /. i)

then A18: F . i = f . i by FUNCT_1:47;

len f <= len F by A2, A15, NAT_1:12;

then A19: dom f c= dom F by FINSEQ_3:30;

then i in dom F by A17;

then i in dom G by A3, FINSEQ_3:29;

then A20: G /. i = G . i by PARTFUN1:def 6;

i in dom h by A15, A6, A17, FINSEQ_3:29;

then A21: H . i = h . i by FUNCT_1:47;

F /. i = F . i by A17, A19, PARTFUN1:def 6;

then A22: f /. i = F /. i by A17, A18, PARTFUN1:def 6;

A23: i in dom g by A15, A16, A17, FINSEQ_3:29;

then G . i = g . i by FUNCT_1:47;

then g /. i = G /. i by A23, A20, PARTFUN1:def 6;

hence h . i = (f /. i) + (g /. i) by A5, A17, A21, A19, A22; :: thesis: verum

F = f ^ <*v*> by A2, FINSEQ_3:55;

then A25: Sum F = (Sum f) + (Sum <*v*>) by RLVECT_1:41;

A26: Sum <*u*> = u by RLVECT_1:44;

H = h ^ <*w*> by A2, A4, FINSEQ_3:55;

hence Sum H = (Sum h) + (Sum <*w*>) by RLVECT_1:41

.= ((Sum f) + (Sum g)) + (v + u) by A24, A12, RLVECT_1:44

.= (((Sum f) + (Sum g)) + v) + u by RLVECT_1:def 3

.= ((Sum F) + (Sum g)) + u by A25, A14, RLVECT_1:def 3

.= (Sum F) + (Sum G) by A13, A26, RLVECT_1:def 3 ;

:: thesis: verum

S

A28: S

proof

for k being Nat holds S
let F, G, H be FinSequence of the carrier of V; :: thesis: ( len F = 0 & len F = len G & len F = len H & ( for k being Nat st k in dom F holds

H . k = (F /. k) + (G /. k) ) implies Sum H = (Sum F) + (Sum G) )

assume that

A29: len F = 0 and

A30: len F = len G and

A31: len F = len H ; :: thesis: ( ex k being Nat st

( k in dom F & not H . k = (F /. k) + (G /. k) ) or Sum H = (Sum F) + (Sum G) )

A32: Sum H = 0. V by A29, A31, RLVECT_1:75;

( Sum F = 0. V & Sum G = 0. V ) by A29, A30, RLVECT_1:75;

hence ( ex k being Nat st

( k in dom F & not H . k = (F /. k) + (G /. k) ) or Sum H = (Sum F) + (Sum G) ) by A32; :: thesis: verum

end;H . k = (F /. k) + (G /. k) ) implies Sum H = (Sum F) + (Sum G) )

assume that

A29: len F = 0 and

A30: len F = len G and

A31: len F = len H ; :: thesis: ( ex k being Nat st

( k in dom F & not H . k = (F /. k) + (G /. k) ) or Sum H = (Sum F) + (Sum G) )

A32: Sum H = 0. V by A29, A31, RLVECT_1:75;

( Sum F = 0. V & Sum G = 0. V ) by A29, A30, RLVECT_1:75;

hence ( ex k being Nat st

( k in dom F & not H . k = (F /. k) + (G /. k) ) or Sum H = (Sum F) + (Sum G) ) by A32; :: thesis: verum

hence for F, G, H being FinSequence of the carrier of V st len F = len G & len F = len H & ( for k being Nat st k in dom F holds

H . k = (F /. k) + (G /. k) ) holds

Sum H = (Sum F) + (Sum G) ; :: thesis: verum