let seq, seq9 be Real_Sequence; :: thesis: ( seq is convergent & seq9 is convergent & ( for n being Element of NAT holds seq . n <= seq9 . n ) implies lim seq <= lim seq9 )
assume that
A1: seq is convergent and
A2: seq9 is convergent and
A3: for n being Element of NAT holds seq . n <= seq9 . n ; :: thesis: lim seq <= lim seq9
A4: seq9 - seq is convergent by A1, A2, Th25;

now

let n be Element of NAT ; :: thesis: 0 <= (seq9 - seq) . n
seq . n <= seq9 . n by A3;
then A5: (seq . n) - (seq . n) <= (seq9 . n) - (seq . n) by XREAL_1:11;
(seq9 - seq) . n = (seq9 . n) + ((- seq) . n) by SEQ_1:11
.= (seq9 . n) + (- (seq . n)) by SEQ_1:14
.= (seq9 . n) - (seq . n) ;
hence 0 <= (seq9 - seq) . n by A5; :: thesis: verum

end;

then A6: 0 <= lim (seq9 - seq) by A4, Th31;
lim (seq9 - seq) = (lim seq9) - (lim seq) by A1, A2, Th26;
then 0 + (lim seq) <= ((lim seq9) - (lim seq)) + (lim seq) by A6, XREAL_1:8;
hence lim seq <= lim seq9 ; :: thesis: verum