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 ; :: 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 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) + () 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 ;
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 ;
then A12: i + 1 in dom F by FINSEQ_1:def 3;
f9 . (i + 1) = f . (i + 1) by ;
then f9 . (i + 1) = (f9 . i) + (F . (i + 1)) by A3, A9, A10;
hence f9 . (i + 1) = (f9 . i) + ((F ^ <*x*>) . (i + 1)) by ; :: 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 ; :: 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 () holds
f . (i + 1) = (f . i) + (() . (i + 1)) ) )

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

thus for i being Element of NAT st i < len () holds
f . (i + 1) = (f . i) + (() . (i + 1)) ; :: thesis: verum
end;
for F being FinSequence of ExtREAL holds S1[F] from 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 ; :: thesis: verum