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 A16: g1 = f1 . (len F) and
A17: f1 . 0 = 0. and
A18: 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 A19: g2 = f2 . (len F) and
A20: f2 . 0 = 0. and
A21: 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 );
A22: S₁[ 0 ] by A17, A20;
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 i < len F by NAT_1:13;
then ( f1 . (i + 1) = (f1 . i) + (F . (i + 1)) & f2 . (i + 1) = (f2 . i) + (F . (i + 1)) & f1 . i = f2 . i ) by A18, A21, A24;
hence f1 . (i + 1) = f2 . (i + 1) ; :: thesis: verum

end;

end;

for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A22, A23);
hence g1 = g2 by A16, A19; :: thesis: verum