let g1, g2 be Element of ExtREAL ; :: thesis: ( ex f being Function of NAT ,ExtREAL st
( g1 = f . (len F) & f . 0 = 0. & ( for i being Element of NAT st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) ) & ex f being Function of NAT ,ExtREAL st
( g2 = f . (len F) & f . 0 = 0. & ( for i being Element of NAT st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) ) implies g1 = g2 )
given f1 being Function of NAT ,ExtREAL such that A17: g1 = f1 . (len F) and
A18: f1 . 0 = 0. and
A19: for i being Element of NAT st i < len F holds
f1 . (i + 1) = (f1 . i) + (F . (i + 1)) ; :: thesis: ( for f being Function of NAT ,ExtREAL holds
( not g2 = f . (len F) or not f . 0 = 0. or ex i being Element of NAT st
( i < len F & not f . (i + 1) = (f . i) + (F . (i + 1)) ) ) or g1 = g2 )
given f2 being Function of NAT ,ExtREAL such that A20: g2 = f2 . (len F) and
A21: f2 . 0 = 0. and
A22: for i being Element of NAT st i < len F holds
f2 . (i + 1) = (f2 . i) + (F . (i + 1)) ; :: thesis: g1 = g2
defpred S₁[ Element of NAT ] means ( $1 <= len F implies f1 . $1 = f2 . $1 );
A23: for i being Element of NAT st S₁[i] holds
S₁[i + 1]

proof

let i be Element of NAT ; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A24: S₁[i] ; :: thesis: S₁[i + 1]
thus S₁[i + 1] :: thesis: verum

proof

assume i + 1 <= len F ; :: thesis: f1 . (i + 1) = f2 . (i + 1)
then A25: i < len F by NAT_1:13;
then f1 . (i + 1) = (f1 . i) + (F . (i + 1)) by A19;
hence f1 . (i + 1) = f2 . (i + 1) by A22, A24, A25; :: thesis: verum

end;

end;

A26: S₁[ 0 ] by A18, A21;
for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A26, A23);
hence g1 = g2 by A17, A20; :: thesis: verum