let V be non empty addLoopStr ; :: thesis: for F, G being FinSequence of the carrier of V
for v being Element of V st len F = (len G) + 1 & G = F | (dom G) & v = F . (len F) holds
Sum F = (Sum G) + v
let F, G be FinSequence of the carrier of V; :: thesis: for v being Element of V st len F = (len G) + 1 & G = F | (dom G) & v = F . (len F) holds
Sum F = (Sum G) + v
let v be Element of V; :: thesis: ( len F = (len G) + 1 & G = F | (dom G) & v = F . (len F) implies Sum F = (Sum G) + v )
assume that
A1: len F = (len G) + 1 and
A2: G = F | (dom G) and
A3: v = F . (len F) ; :: thesis: Sum F = (Sum G) + v
consider f being Function of NAT ,the carrier of V such that
A4: Sum F = f . (len F) and
A5: f . 0 = 0. V and
A6: for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f . (j + 1) = (f . j) + v by Def13;
consider g being Function of NAT ,the carrier of V such that
A7: Sum G = g . (len G) and
A8: g . 0 = 0. V and
A9: for j being Element of NAT
for v being Element of V st j < len G & v = G . (j + 1) holds
g . (j + 1) = (g . j) + v by Def13;
defpred S₁[ Element of NAT ] means for H being FinSequence of the carrier of V st len H = $1 & H = F | (Seg $1) & len H <= len G holds
f . (len H) = g . (len H);
A10: S₁[ 0 ] by A5, A8;
A11: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

now

let k be Element of NAT ; :: thesis: ( ( for H being FinSequence of the carrier of V st len H = k & H = F | (Seg k) & len H <= len G holds
f . (len H) = g . (len H) ) implies for H being FinSequence of the carrier of V st len H = k + 1 & H = F | (Seg (k + 1)) & len H <= len G holds
f . (len H) = g . (len H) )
assume A12: for H being FinSequence of the carrier of V st len H = k & H = F | (Seg k) & len H <= len G holds
f . (len H) = g . (len H) ; :: thesis: for H being FinSequence of the carrier of V st len H = k + 1 & H = F | (Seg (k + 1)) & len H <= len G holds
f . (len H) = g . (len H)
let H be FinSequence of the carrier of V; :: thesis: ( len H = k + 1 & H = F | (Seg (k + 1)) & len H <= len G implies f . (len H) = g . (len H) )
assume that
A13: len H = k + 1 and
A14: H = F | (Seg (k + 1)) and
A15: len H <= len G ; :: thesis: f . (len H) = g . (len H)
reconsider p = H | (Seg k) as FinSequence of the carrier of V by FINSEQ_1:23;
( 1 <= k + 1 & k + 1 <= len F ) by A1, A13, A15, NAT_1:12;
then k + 1 in Seg (len F) by FINSEQ_1:3;
then reconsider v = F . (k + 1) as Element of V by Th54;
A16: k <= len H by A13, NAT_1:12;
then A17: len p = k by FINSEQ_1:21;
Seg k c= Seg (k + 1) by A13, A16, FINSEQ_1:7;
then A18: p = F | (Seg k) by A14, FUNCT_1:82;
( k <= len G & len G < len F ) by A1, A15, A16, XREAL_1:31, XXREAL_0:2;
then A19: k < len F by XXREAL_0:2;
( 1 <= k + 1 & k + 1 <= len G ) by A13, A15, NAT_1:12;
then k + 1 in Seg (len G) by FINSEQ_1:3;
then k + 1 in dom G by FINSEQ_1:def 3;
then A20: v = G . (k + 1) by A2, FUNCT_1:70;
k < k + 1 by XREAL_1:31;
then k < len G by A13, A15, XXREAL_0:2;
then ( f . (k + 1) = (f . k) + v & g . (k + 1) = (g . k) + v ) by A6, A9, A19, A20;
hence f . (len H) = g . (len H) by A12, A13, A15, A16, A17, A18, XXREAL_0:2; :: thesis: verum

end;

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

end;

A21: dom G = Seg (len G) by FINSEQ_1:def 3;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A10, A11);
then f . (len G) = g . (len G) by A2, A21;
hence Sum F = (Sum G) + v by A1, A3, A4, A6, A7, XREAL_1:31; :: thesis: verum