defpred S_{1}[ FinSequence of ExtREAL ] means ex f being sequence of ExtREAL st

( f . 0 = 0. & ( for i being Element of NAT st i < len $1 holds

f . (i + 1) = (f . i) + ($1 . (i + 1)) ) );

A1: for F being FinSequence of ExtREAL

for x being Element of ExtREAL st S_{1}[F] holds

S_{1}[F ^ <*x*>]
_{1}[ <*> ExtREAL]
_{1}[F]
from FINSEQ_2:sch 2(A14, A1);

then consider f being sequence of ExtREAL such that

A15: f . 0 = 0. and

A16: for i being Element of NAT st i < len F holds

f . (i + 1) = (f . i) + (F . (i + 1)) ;

A17: for i being Nat st i < len F holds

f . (i + 1) = (f . i) + (F . (i + 1))

( f . (len F) = f . (len F) & f . 0 = 0. & ( for i being Nat st i < len F holds

f . (i + 1) = (f . i) + (F . (i + 1)) ) )

thus ex f being sequence of ExtREAL st

( f . (len F) = f . (len F) & f . 0 = 0. & ( for i being Nat st i < len F holds

f . (i + 1) = (f . i) + (F . (i + 1)) ) ) by A15, A17; :: thesis: verum

( f . 0 = 0. & ( for i being Element of NAT st i < len $1 holds

f . (i + 1) = (f . i) + ($1 . (i + 1)) ) );

A1: for F being FinSequence of ExtREAL

for x being Element of ExtREAL st S

S

proof

A14:
S
let F be FinSequence of ExtREAL ; :: thesis: for x being Element of ExtREAL st S_{1}[F] holds

S_{1}[F ^ <*x*>]

let x be Element of ExtREAL ; :: thesis: ( S_{1}[F] implies S_{1}[F ^ <*x*>] )

assume S_{1}[F]
; :: thesis: S_{1}[F ^ <*x*>]

then consider f being sequence of ExtREAL such that

A2: f . 0 = 0. and

A3: for i being Element of NAT st i < len F holds

f . (i + 1) = (f . i) + (F . (i + 1)) ;

defpred S_{2}[ Element of NAT , set ] means ( ( $1 <= len F implies $2 = f . $1 ) & ( $1 = (len F) + 1 implies $2 = (f . (len F)) + x ) );

A4: for i being Element of NAT ex g being Element of ExtREAL st S_{2}[i,g]

A7: for i being Element of NAT holds S_{2}[i,f9 . i]
from FUNCT_2:sch 3(A4);

thus S_{1}[F ^ <*x*>]
:: thesis: verum

end;S

let x be Element of ExtREAL ; :: thesis: ( S

assume S

then consider f being sequence of ExtREAL such that

A2: f . 0 = 0. and

A3: for i being Element of NAT st i < len F holds

f . (i + 1) = (f . i) + (F . (i + 1)) ;

defpred S

A4: for i being Element of NAT ex g being Element of ExtREAL st S

proof

consider f9 being sequence of ExtREAL such that
let i be Element of NAT ; :: thesis: ex g being Element of ExtREAL st S_{2}[i,g]

end;A7: for i being Element of NAT holds S

thus S

proof

take
f9
; :: thesis: ( f9 . 0 = 0. & ( for i being Element of NAT st i < len (F ^ <*x*>) holds

f9 . (i + 1) = (f9 . i) + ((F ^ <*x*>) . (i + 1)) ) )

thus f9 . 0 = 0. by A2, A7; :: thesis: for i being Element of NAT st i < len (F ^ <*x*>) holds

f9 . (i + 1) = (f9 . i) + ((F ^ <*x*>) . (i + 1))

thus for i being Element of NAT st i < len (F ^ <*x*>) holds

f9 . (i + 1) = (f9 . i) + ((F ^ <*x*>) . (i + 1)) :: thesis: verum

end;f9 . (i + 1) = (f9 . i) + ((F ^ <*x*>) . (i + 1)) ) )

thus f9 . 0 = 0. by A2, A7; :: thesis: for i being Element of NAT st i < len (F ^ <*x*>) holds

f9 . (i + 1) = (f9 . i) + ((F ^ <*x*>) . (i + 1))

thus for i being Element of NAT st i < len (F ^ <*x*>) holds

f9 . (i + 1) = (f9 . i) + ((F ^ <*x*>) . (i + 1)) :: thesis: verum

proof

let i be Element of NAT ; :: thesis: ( i < len (F ^ <*x*>) implies f9 . (i + 1) = (f9 . i) + ((F ^ <*x*>) . (i + 1)) )

assume i < len (F ^ <*x*>) ; :: thesis: f9 . (i + 1) = (f9 . i) + ((F ^ <*x*>) . (i + 1))

then i < (len F) + (len <*x*>) by FINSEQ_1:22;

then i < (len F) + 1 by FINSEQ_1:39;

then A8: i <= len F by NAT_1:13;

then A9: f9 . i = f . i by A7;

end;assume i < len (F ^ <*x*>) ; :: thesis: f9 . (i + 1) = (f9 . i) + ((F ^ <*x*>) . (i + 1))

then i < (len F) + (len <*x*>) by FINSEQ_1:22;

then i < (len F) + 1 by FINSEQ_1:39;

then A8: i <= len F by NAT_1:13;

then A9: f9 . i = f . i by A7;

per cases
( i < len F or i = len F )
by A8, XXREAL_0:1;

end;

suppose A10:
i < len F
; :: thesis: f9 . (i + 1) = (f9 . i) + ((F ^ <*x*>) . (i + 1))

then A11:
i + 1 <= len F
by INT_1:7;

1 <= i + 1 by NAT_1:12;

then i + 1 in Seg (len F) by A11, FINSEQ_1:1;

then A12: i + 1 in dom F by FINSEQ_1:def 3;

f9 . (i + 1) = f . (i + 1) by A7, A11;

then f9 . (i + 1) = (f9 . i) + (F . (i + 1)) by A3, A9, A10;

hence f9 . (i + 1) = (f9 . i) + ((F ^ <*x*>) . (i + 1)) by A12, FINSEQ_1:def 7; :: thesis: verum

end;1 <= i + 1 by NAT_1:12;

then i + 1 in Seg (len F) by A11, FINSEQ_1:1;

then A12: i + 1 in dom F by FINSEQ_1:def 3;

f9 . (i + 1) = f . (i + 1) by A7, A11;

then f9 . (i + 1) = (f9 . i) + (F . (i + 1)) by A3, A9, A10;

hence f9 . (i + 1) = (f9 . i) + ((F ^ <*x*>) . (i + 1)) by A12, FINSEQ_1:def 7; :: thesis: verum

proof

for F being FinSequence of ExtREAL holds S
reconsider f = NAT --> 0. as sequence of ExtREAL ;

take f ; :: thesis: ( f . 0 = 0. & ( for i being Element of NAT st i < len (<*> ExtREAL) holds

f . (i + 1) = (f . i) + ((<*> ExtREAL) . (i + 1)) ) )

thus f . 0 = 0. by FUNCOP_1:7; :: thesis: for i being Element of NAT st i < len (<*> ExtREAL) holds

f . (i + 1) = (f . i) + ((<*> ExtREAL) . (i + 1))

thus for i being Element of NAT st i < len (<*> ExtREAL) holds

f . (i + 1) = (f . i) + ((<*> ExtREAL) . (i + 1)) ; :: thesis: verum

end;take f ; :: thesis: ( f . 0 = 0. & ( for i being Element of NAT st i < len (<*> ExtREAL) holds

f . (i + 1) = (f . i) + ((<*> ExtREAL) . (i + 1)) ) )

thus f . 0 = 0. by FUNCOP_1:7; :: thesis: for i being Element of NAT st i < len (<*> ExtREAL) holds

f . (i + 1) = (f . i) + ((<*> ExtREAL) . (i + 1))

thus for i being Element of NAT st i < len (<*> ExtREAL) holds

f . (i + 1) = (f . i) + ((<*> ExtREAL) . (i + 1)) ; :: thesis: verum

then consider f being sequence of ExtREAL such that

A15: f . 0 = 0. and

A16: for i being Element of NAT st i < len F holds

f . (i + 1) = (f . i) + (F . (i + 1)) ;

A17: for i being Nat st i < len F holds

f . (i + 1) = (f . i) + (F . (i + 1))

proof

take
f . (len F)
; :: thesis: ex f being sequence of ExtREAL st
let i be Nat; :: thesis: ( i < len F implies f . (i + 1) = (f . i) + (F . (i + 1)) )

i in NAT by ORDINAL1:def 12;

hence ( i < len F implies f . (i + 1) = (f . i) + (F . (i + 1)) ) by A16; :: thesis: verum

end;i in NAT by ORDINAL1:def 12;

hence ( i < len F implies f . (i + 1) = (f . i) + (F . (i + 1)) ) by A16; :: thesis: verum

( f . (len F) = f . (len F) & f . 0 = 0. & ( for i being Nat st i < len F holds

f . (i + 1) = (f . i) + (F . (i + 1)) ) )

thus ex f being sequence of ExtREAL st

( f . (len F) = f . (len F) & f . 0 = 0. & ( for i being Nat st i < len F holds

f . (i + 1) = (f . i) + (F . (i + 1)) ) ) by A15, A17; :: thesis: verum