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 Element of NAT st k in dom F holds
H . k = (F /. k) + (G /. k) ) holds
Sum H = (Sum F) + (Sum G)
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);

now

let k be Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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

let i be Element of 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;

then A24: Sum h = (Sum f) + (Sum g) by A1, A15, A16, A6;
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;

then A27: for k being Element of NAT st S₁[k] holds
S₁[k + 1] ;
A28: S₁[ 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 Element of 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 Element of 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 Element of NAT st
( k in dom F & not H . k = (F /. k) + (G /. k) ) or Sum H = (Sum F) + (Sum G) ) by A32, RLVECT_1:4; :: thesis: verum

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(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 Element of NAT st k in dom F holds
H . k = (F /. k) + (G /. k) ) holds
Sum H = (Sum F) + (Sum G) ; :: thesis: verum