let V be non empty addLoopStr ; :: thesis: for v being Element of V
for F, G being FinSequence 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: for F, G being FinSequence 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 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 g being sequence of V such that
A4: Sum G = g . (len G) and
A5: g . 0 = 0. V and
A6: for j being Nat
for v being Element of V st j < len G & v = G . (j + 1) holds
g . (j + 1) = (g . j) + v by Def12;
consider f being sequence of V such that
A7: Sum F = f . (len F) and
A8: f . 0 = 0. V and
A9: for j being Nat
for v being Element of V st j < len F & v = F . (j + 1) holds
f . (j + 1) = (f . j) + v by Def12;
defpred S₁[ Nat] means for H being FinSequence of V st len H = $1 & H = F | (Seg $1) & len H <= len G holds
f . (len H) = g . (len H);

now :: thesis: for k being Nat st ( for H being FinSequence of V st len H = k & H = F | (Seg k) & len H <= len G holds
f . (len H) = g . (len H) ) holds
for H being FinSequence of V st len H = k + 1 & H = F | (Seg (k + 1)) & len H <= len G holds
f . (len H) = g . (len H)

let k be Nat; :: thesis: ( ( for H being FinSequence 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 V st len H = k + 1 & H = F | (Seg (k + 1)) & len H <= len G holds
f . (len H) = g . (len H) )
assume A10: for H being FinSequence 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 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 V; :: thesis: ( len H = k + 1 & H = F | (Seg (k + 1)) & len H <= len G implies f . (len H) = g . (len H) )
assume that
A11: len H = k + 1 and
A12: H = F | (Seg (k + 1)) and
A13: len H <= len G ; :: thesis: f . (len H) = g . (len H)
( 1 <= k + 1 & k + 1 <= len F ) by A1, A11, A13, NAT_1:12;
then k + 1 in dom F by FINSEQ_3:25;
then reconsider v = F . (k + 1) as Element of V by FUNCT_1:102;
1 <= k + 1 by NAT_1:12;
then k + 1 in Seg (len G) by A11, A13, FINSEQ_1:1;
then k + 1 in dom G by FINSEQ_1:def 3;
then A14: v = G . (k + 1) by A2, FUNCT_1:47;
reconsider H1 = H as FinSequence of V ;
reconsider p = H1 | (Seg k) as FinSequence of V by FINSEQ_1:18;
A15: k <= len H by A11, NAT_1:12;
then Seg k c= Seg (k + 1) by A11, FINSEQ_1:5;
then A16: p = F | (Seg k) by A12, FUNCT_1:51;
k < k + 1 by XREAL_1:29;
then k < len G by A11, A13, XXREAL_0:2;
then A17: g . (k + 1) = (g . k) + v by A6, A14;
A18: len G < len F by A1, XREAL_1:29;
k <= len G by A13, A15, XXREAL_0:2;
then k < len F by A18, XXREAL_0:2;
then A19: f . (k + 1) = (f . k) + v by A9;
len p = k by A15, FINSEQ_1:17;
hence f . (len H) = g . (len H) by A10, A11, A13, A15, A16, A19, A17, XXREAL_0:2; :: thesis: verum

end;

then A20: for k being Nat st S₁[k] holds
S₁[k + 1] ;
A21: dom G = Seg (len G) by FINSEQ_1:def 3;
A22: S₁[ 0 ] by A8, A5;
for k being Nat holds S₁[k] from NAT_1:sch 2(A22, A20);
then f . (len G) = g . (len G) by A2, A21;
hence Sum F = (Sum G) + v by A1, A3, A7, A9, A4, XREAL_1:29; :: thesis: verum