let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis:
defpred S₁[ Element of 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 Element of NAT st k in dom F holds
H . k = (F /. k) + (G /. k) ) holds
Sum H = (Sum F) + (Sum G);
A1: S₁[ 0 ]

let F, G, H be FinSequence of the carrier of V; :: thesis:
assume ( len F = 0 & len F = len G & len F = len H ) ; :: thesis:
then ( Sum F = 0. V & Sum G = 0. V & Sum H = 0. V & (0. V) + (0. V) = 0. V ) by RLVECT_1:10, RLVECT_1:94;
hence ( ex k being Element of NAT st
( k in dom F & not H . k = (F /. k) + (G /. k) ) or Sum H = (Sum F) + (Sum G) ) ; :: thesis:

end;

A2: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

let k be Element of NAT ; :: thesis:
assume A3: 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 Element of NAT st k in dom F holds
H . k = (F /. k) + (G /. k) ) holds
Sum H = (Sum F) + (Sum G) ; :: thesis:
let F, G, H be FinSequence of the carrier of V; :: thesis:
assume that
A4: len F = k + 1 and
A5: len F = len G and
A6: len F = len H and
A7: for k being Element of NAT st k in dom F holds
H . k = (F /. k) + (G /. k) ; :: thesis:
reconsider f = F | (Seg k), g = G | (Seg k), h = H | (Seg k) as FinSequence of the carrier of V by FINSEQ_1:23;
A8: ( len f = k & len g = k & len h = k ) by A4, A5, A6, FINSEQ_3:59;

let i be Element of NAT ; :: thesis:
assume A9: i in dom f ; :: thesis:
then A10: ( i in dom g & i in dom h ) by A8, FINSEQ_3:31;
then A11: ( F . i = f . i & G . i = g . i & H . i = h . i ) by A9, FUNCT_1:70;
len f <= len F by A4, A8, NAT_1:12;
then A12: dom f c= dom F by FINSEQ_3:32;
then i in dom F by A9;
then ( i in dom F & i in dom G ) by A5, FINSEQ_3:31;
then ( F /. i = F . i & G /. i = G . i ) by PARTFUN1:def 8;
then ( f /. i = F /. i & g /. i = G /. i ) by A9, A10, A11, PARTFUN1:def 8;
hence h . i = (f /. i) + (g /. i) by A7, A9, A11, A12; :: thesis:

end;

then A13: Sum h = (Sum f) + (Sum g) by A3, A8;
k + 1 in Seg (k + 1) by FINSEQ_1:6;
then A14: ( k + 1 in dom F & k + 1 in dom G & k + 1 in dom H ) by A4, A5, A6, FINSEQ_1:def 3;
then ( F . (k + 1) in rng F & G . (k + 1) in rng G & H . (k + 1) in rng H & rng F c= the carrier of V & rng G c= the carrier of V & rng H c= the carrier of V ) by FUNCT_1:def 5;
then reconsider v = F . (k + 1), u = G . (k + 1), w = H . (k + 1) as Element of V ;
A15: ( G = g ^ <*u*> & F = f ^ <*v*> & H = h ^ <*w*> ) by A4, A5, A6, FINSEQ_3:61;
then A16: ( Sum G = (Sum g) + (Sum <*u*>) & Sum F = (Sum f) + (Sum <*v*>) & Sum <*v*> = v & Sum <*u*> = u ) by RLVECT_1:58, RLVECT_1:61;
A17: w = (F /. (k + 1)) + (G /. (k + 1)) by A7, A14
.= v + (G /. (k + 1)) by A14, PARTFUN1:def 8
.= v + u by A14, PARTFUN1:def 8 ;
thus Sum H = (Sum h) + (Sum <*w*>) by A15, RLVECT_1:58
.= ((Sum f) + (Sum g)) + (v + u) by A13, A17, RLVECT_1:61
.= (((Sum f) + (Sum g)) + v) + u by RLVECT_1:def 6
.= ((Sum F) + (Sum g)) + u by A16, RLVECT_1:def 6
.= (Sum F) + (Sum G) by A16, RLVECT_1:def 6 ; :: thesis:

end;

hence for k being Element of NAT st S₁[k] holds
S₁[k + 1] ; :: thesis:

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A1, A2);
hence for F, G, H being FinSequence of the carrier of V st len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
H . k = (F /. k) + (G /. k) ) holds
Sum H = (Sum F) + (Sum G) ; :: thesis: