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 S1[ 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);
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)
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 ;
A7: k + 1 in Seg (k + 1) by FINSEQ_1:4;
then A8: k + 1 in dom G by ;
then A9: G . (k + 1) in rng G by FUNCT_1:def 3;
k + 1 in dom H by ;
then A10: H . (k + 1) in rng H by FUNCT_1:def 3;
A11: k + 1 in dom F by ;
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 ;
A12: w = (F /. (k + 1)) + (G /. (k + 1)) by
.= v + (G /. (k + 1)) by
.= v + u by ;
G = g ^ <*u*> by ;
then A13: Sum G = (Sum g) + () by RLVECT_1:41;
A14: Sum <*v*> = v by RLVECT_1:44;
A15: len f = k by ;
A16: len g = k by ;
now :: thesis: for i being Nat st i in dom f holds
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 ;
then A19: dom f c= dom F by FINSEQ_3:30;
then i in dom F by A17;
then i in dom G by ;
then A20: G /. i = G . i by PARTFUN1:def 6;
i in dom h by ;
then A21: H . i = h . i by FUNCT_1:47;
F /. i = F . i by ;
then A22: f /. i = F /. i by ;
A23: i in dom g by ;
then G . i = g . i by FUNCT_1:47;
then g /. i = G /. i by ;
hence h . i = (f /. i) + (g /. i) by A5, A17, A21, A19, A22; :: thesis: verum
end;
then A24: Sum h = (Sum f) + (Sum g) by A1, A15, A16, A6;
F = f ^ <*v*> by ;
then A25: Sum F = (Sum f) + () by RLVECT_1:41;
A26: Sum <*u*> = u by RLVECT_1:44;
H = h ^ <*w*> by ;
hence Sum H = (Sum h) + () by RLVECT_1:41
.= ((Sum f) + (Sum g)) + (v + u) by
.= (((Sum f) + (Sum g)) + v) + u by RLVECT_1:def 3
.= ((Sum F) + (Sum g)) + u by
.= (Sum F) + (Sum G) by ;
:: thesis: verum
end;
then A27: for k being Nat st S1[k] holds
S1[k + 1] ;
A28: S1[ 0 ]
proof
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 ;
( Sum F = 0. V & Sum G = 0. V ) by ;
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;
for k being Nat holds S1[k] from 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