defpred S1[ 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 S1[F] holds
S1[F ^ <*x*>]
proof
let F be FinSequence of ExtREAL ; :: thesis: for x being Element of ExtREAL st S1[F] holds
S1[F ^ <*x*>]
let x be Element of ExtREAL ; :: thesis: ( S1[F] implies S1[F ^ <*x*>] )
assume S1[F] ; :: thesis: S1[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 S2[ 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 S2[i,g]
proof
let i be Element of NAT ; :: thesis: ex g being Element of ExtREAL st S2[i,g]
per cases ( i <> (len F) + 1 or i = (len F) + 1 ) ;
suppose A5: i <> (len F) + 1 ; :: thesis: ex g being Element of ExtREAL st S2[i,g]
take f . i ; :: thesis: S2[i,f . i]
thus S2[i,f . i] by A5; :: thesis: verum
end;
suppose A6: i = (len F) + 1 ; :: thesis: ex g being Element of ExtREAL st S2[i,g]
take (f . (len F)) + x ; :: thesis: S2[i,(f . (len F)) + x]
thus S2[i,(f . (len F)) + x] by A6, NAT_1:13; :: thesis: verum
end;
end;
end;
consider f9 being sequence of ExtREAL such that
A7: for i being Element of NAT holds S2[i,f9 . i] from FUNCT_2:sch 3(A4);
 thus S1[F ^ <*x*>] :: thesis: verum
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
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;
per cases ( i < len F or i = len F ) by A8, XXREAL_0:1;
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;
suppose A13: i = len F ; :: thesis: f9 . (i + 1) = (f9 . i) + ((F ^ <*x*>) . (i + 1))
then f9 . (i + 1) = (f9 . i) + x by A7, A9;
hence f9 . (i + 1) = (f9 . i) + ((F ^ <*x*>) . (i + 1)) by A13, FINSEQ_1:42; :: thesis: verum
end;
end;
end;
end;
end;
A14: S1[ <*> ExtREAL]
proof
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;
for F being FinSequence of ExtREAL holds S1[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))
proof
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;
take f . (len F) ; :: thesis: 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)) ) )
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