let x0 be Real; :: thesis:
let seq be Real_Sequence; :: thesis:
let f be PartFunc of REAL,REAL; :: thesis:
assume that
A1: for g1 being Real ex r being Real st
( x0 < r & ( for r1 being Real st r1 < r & x0 < r1 & r1 in dom f holds
f . r1 < g1 ) ) and
A2: seq is convergent and
A3: lim seq = x0 and
A4: rng seq c= (dom f) /\ (right_open_halfline x0) ; :: thesis:
A5: (dom f) /\ (right_open_halfline x0) c= dom f by XBOOLE_1:17;

let g1 be Real; :: thesis:
consider r being Real such that
A6: x0 < r and
A7: for r1 being Real st r1 < r & x0 < r1 & r1 in dom f holds
f . r1 < g1 by A1;
consider n being Nat such that
A8: for k being Nat st n <= k holds
seq . k < r by A2, A3, A6, Th2;
take n = n; :: thesis:
let k be Nat; :: thesis:
assume A9: n <= k ; :: thesis:
A10: seq . k in rng seq by VALUED_0:28;
then seq . k in right_open_halfline x0 by A4, XBOOLE_0:def 4;
then seq . k in { g2 where g2 is Real : x0 < g2 } by XXREAL_1:230;
then A11: ex g2 being Real st
( g2 = seq . k & x0 < g2 ) ;
A12: k in NAT by ORDINAL1:def 12;
seq . k in dom f by A4, A10, XBOOLE_0:def 4;
then f . (seq . k) < g1 by A7, A8, A9, A11;
hence (f /* seq) . k < g1 by A4, A5, FUNCT_2:108, XBOOLE_1:1, A12; :: thesis:

end;