let F1, F2 be sequence of ExtREAL; :: thesis:
assume A1: for n being Element of NAT holds F1 . n <= F2 . n ; :: thesis:
for x being ExtReal st x in rng (Ser F1) holds
ex y being ExtReal st
( y in rng (Ser F2) & x <= y )

let x be ExtReal; :: thesis:
A2: dom (Ser F1) = NAT by FUNCT_2:def 1;
assume x in rng (Ser F1) ; :: thesis:
then consider n being object such that
A3: n in NAT and
A4: x = (Ser F1) . n by A2, FUNCT_1:def 3;
reconsider n = n as Element of NAT by A3;
reconsider y = (Ser F2) . n as R_eal ;
take y ; :: thesis:
dom (Ser F2) = NAT by FUNCT_2:def 1;
hence ( y in rng (Ser F2) & x <= y ) by A1, A4, Th41, FUNCT_1:def 3; :: thesis:

end;