let g1, g2 be Element of ExtREAL ; :: thesis: ( ex f being sequence of ExtREAL st
( g1 = f . (len F) & f . 0 = 0. & ( for i being Nat st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) ) & ex f being sequence of ExtREAL st
( g2 = f . (len F) & f . 0 = 0. & ( for i being Nat st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) ) implies g1 = g2 )
given f1 being sequence of ExtREAL such that A18: g1 = f1 . (len F) and
A19: f1 . 0 = 0. and
A20: for i being Nat st i < len F holds
f1 . (i + 1) = (f1 . i) + (F . (i + 1)) ; :: thesis: ( for f being sequence of ExtREAL holds
( not g2 = f . (len F) or not f . 0 = 0. or ex i being Nat st
( i < len F & not f . (i + 1) = (f . i) + (F . (i + 1)) ) ) or g1 = g2 )
given f2 being sequence of ExtREAL such that A21: g2 = f2 . (len F) and
A22: f2 . 0 = 0. and
A23: for i being Nat st i < len F holds
f2 . (i + 1) = (f2 . i) + (F . (i + 1)) ; :: thesis: g1 = g2
defpred S1[ Nat] means ( $1 <= len F implies f1 . $1 = f2 . $1 );
A24: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A25: S1[i] ; :: thesis: S1[i + 1]
thus S1[i + 1] :: thesis: verum
proof
assume i + 1 <= len F ; :: thesis: f1 . (i + 1) = f2 . (i + 1)
then A26: i < len F by NAT_1:13;
then f1 . (i + 1) = (f1 . i) + (F . (i + 1)) by A20;
hence f1 . (i + 1) = f2 . (i + 1) by A23, A25, A26; :: thesis: verum
end;
end;
A27: S1[ 0 ] by A19, A22;
for i being Nat holds S1[i] from NAT_1:sch 2(A27, A24);
 hence g1 = g2 by A18, A21; :: thesis: verum