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 S_{1}[ Nat] means ( $1 <= len F implies f1 . $1 = f2 . $1 );

A24: for i being Nat st S_{1}[i] holds

S_{1}[i + 1]
_{1}[ 0 ]
by A19, A22;

for i being Nat holds S_{1}[i]
from NAT_1:sch 2(A27, A24);

hence g1 = g2 by A18, A21; :: thesis: verum

( 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 S

A24: for i being Nat st S

S

proof

A27:
S
let i be Nat; :: thesis: ( S_{1}[i] implies S_{1}[i + 1] )

assume A25: S_{1}[i]
; :: thesis: S_{1}[i + 1]

thus S_{1}[i + 1]
:: thesis: verum

end;assume A25: S

thus S

for i being Nat holds S

hence g1 = g2 by A18, A21; :: thesis: verum