let seq1, seq2 be ExtREAL_sequence; :: thesis:
assume that
A1: seq1 is convergent and
A2: seq2 is convergent and
A3: for n being Nat holds seq1 . n <= seq2 . n ; :: thesis:

per cases by A1, MESFUNC5:def 11;

suppose A4: seq1 is convergent_to_finite_number ; :: thesis:

A5: not seq2 is convergent_to_-infty

assume A6: seq2 is convergent_to_-infty ; :: thesis:

let g be Real; :: thesis:
assume g < 0 ; :: thesis:
then consider n being Nat such that
A7: for m being Nat st n <= m holds
seq2 . m <= g by A6, MESFUNC5:def 10;

let m be Nat; :: thesis:
A8: seq1 . m <= seq2 . m by A3;
assume n <= m ; :: thesis:
then seq2 . m <= g by A7;
hence seq1 . m <= g by A8, XXREAL_0:2; :: thesis:

end;

hence ex n being Nat st
for m being Nat st n <= m holds
seq1 . m <= g ; :: thesis:

end;

then seq1 is convergent_to_-infty by MESFUNC5:def 10;
hence contradiction by A4, MESFUNC5:51; :: thesis:

end;

per cases by A2, A5, MESFUNC5:def 11;

suppose A9: seq2 is convergent_to_finite_number ; :: thesis:

consider k1 being Nat such that
A10: seq1 ^\ k1 is bounded by A4, Th19;
seq1 ^\ k1 is bounded_above by A10;
then rng (seq1 ^\ k1) is bounded_above ;
then consider UB being Real such that
A11: UB is UpperBound of rng (seq1 ^\ k1) by XXREAL_2:def 10;
consider k2 being Nat such that
A12: seq2 ^\ k2 is bounded by A9, Th19;
reconsider k = max (k1,k2) as Element of NAT by ORDINAL1:def 12;
A13: lim seq2 = lim (seq2 ^\ k) by A9, Th20;
A14: dom (seq1 ^\ k1) = NAT by FUNCT_2:def 1;

reconsider k2 = k - k1 as Element of NAT by INT_1:5, XXREAL_0:25;
let y be object ; :: thesis:
assume y in rng (seq1 ^\ k) ; :: thesis:
then consider n being object such that
A15: n in dom (seq1 ^\ k) and
A16: (seq1 ^\ k) . n = y by FUNCT_1:def 3;
reconsider n = n as Element of NAT by A15;
y = seq1 . (k + n) by A16, NAT_1:def 3;
then y = seq1 . (k1 + (k2 + n)) ;
then y = (seq1 ^\ k1) . (k2 + n) by NAT_1:def 3;
hence y in rng (seq1 ^\ k1) by A14, FUNCT_1:def 3; :: thesis:

end;

then A17: rng (seq1 ^\ k) c= rng (seq1 ^\ k1) ;
then UB is UpperBound of rng (seq1 ^\ k) by A11, XXREAL_2:6;
then rng (seq1 ^\ k) is bounded_above by XXREAL_2:def 10;
then A18: seq1 ^\ k is bounded_above ;
seq1 ^\ k1 is bounded_below by A10;
then rng (seq1 ^\ k1) is bounded_below ;
then consider LB being Real such that
A19: LB is LowerBound of rng (seq1 ^\ k1) by XXREAL_2:def 9;
LB is LowerBound of rng (seq1 ^\ k) by A17, A19, XXREAL_2:5;
then rng (seq1 ^\ k) is bounded_below by XXREAL_2:def 9;
then seq1 ^\ k is bounded_below ;
then seq1 ^\ k is bounded by A18;
then reconsider rseq1 = seq1 ^\ k as Real_Sequence by Th11;
seq2 ^\ k2 is bounded_below by A12;
then rng (seq2 ^\ k2) is bounded_below ;
then consider LB being Real such that
A20: LB is LowerBound of rng (seq2 ^\ k2) by XXREAL_2:def 9;
A21: lim seq1 = lim (seq1 ^\ k) by A4, Th20;
seq2 ^\ k2 is bounded_above by A12;
then rng (seq2 ^\ k2) is bounded_above ;
then consider UB being Real such that
A22: UB is UpperBound of rng (seq2 ^\ k2) by XXREAL_2:def 10;
A23: dom (seq2 ^\ k2) = NAT by FUNCT_2:def 1;

reconsider k3 = k - k2 as Element of NAT by INT_1:5, XXREAL_0:25;
let y be object ; :: thesis:
assume y in rng (seq2 ^\ k) ; :: thesis:
then consider n being object such that
A24: n in dom (seq2 ^\ k) and
A25: (seq2 ^\ k) . n = y by FUNCT_1:def 3;
reconsider n = n as Element of NAT by A24;
y = seq2 . (k + n) by A25, NAT_1:def 3;
then y = seq2 . (k2 + (k3 + n)) ;
then y = (seq2 ^\ k2) . (k3 + n) by NAT_1:def 3;
hence y in rng (seq2 ^\ k2) by A23, FUNCT_1:def 3; :: thesis:

end;

then A26: rng (seq2 ^\ k) c= rng (seq2 ^\ k2) ;
then UB is UpperBound of rng (seq2 ^\ k) by A22, XXREAL_2:6;
then rng (seq2 ^\ k) is bounded_above by XXREAL_2:def 10;
then A27: seq2 ^\ k is bounded_above ;
LB is LowerBound of rng (seq2 ^\ k) by A20, A26, XXREAL_2:5;
then rng (seq2 ^\ k) is bounded_below by XXREAL_2:def 9;
then seq2 ^\ k is bounded_below ;
then seq2 ^\ k is bounded by A27;
then reconsider rseq2 = seq2 ^\ k as Real_Sequence by Th11;
A28: seq2 ^\ k is convergent_to_finite_number by A9, Th20;
then A29: rseq2 is convergent by Th15;
A30: for n being Nat holds rseq1 . n <= rseq2 . n

let n be Nat; :: thesis:
A31: (seq2 ^\ k) . n = seq2 . (k + n) by NAT_1:def 3;
(seq1 ^\ k) . n = seq1 . (k + n) by NAT_1:def 3;
hence rseq1 . n <= rseq2 . n by A3, A31; :: thesis:

end;

A32: seq1 ^\ k is convergent_to_finite_number by A4, Th20;
then A33: lim (seq1 ^\ k) = lim rseq1 by Th15;
A34: lim (seq2 ^\ k) = lim rseq2 by A28, Th15;
rseq1 is convergent by A32, Th15;
hence lim seq1 <= lim seq2 by A29, A33, A34, A30, A21, A13, SEQ_2:18; :: thesis:

end;

suppose A35: seq2 is convergent_to_+infty ; :: thesis:

then seq2 is convergent by MESFUNC5:def 11;
then lim seq2 = +infty by A35, MESFUNC5:def 12;
hence lim seq1 <= lim seq2 by XXREAL_0:3; :: thesis:

end;

end;

end;

suppose A36: seq1 is convergent_to_+infty ; :: thesis:

let g be Real; :: thesis:
assume 0 < g ; :: thesis:
then consider n being Nat such that
A37: for m being Nat st n <= m holds
g <= seq1 . m by A36, MESFUNC5:def 9;

let m be Nat; :: thesis:
A38: seq1 . m <= seq2 . m by A3;
assume n <= m ; :: thesis:
then g <= seq1 . m by A37;
hence g <= seq2 . m by A38, XXREAL_0:2; :: thesis:

end;

hence ex n being Nat st
for m being Nat st n <= m holds
g <= seq2 . m ; :: thesis:

end;

then A39: seq2 is convergent_to_+infty by MESFUNC5:def 9;
then seq2 is convergent by MESFUNC5:def 11;
then lim seq2 = +infty by A39, MESFUNC5:def 12;
hence lim seq1 <= lim seq2 by XXREAL_0:3; :: thesis:

end;

suppose A40: seq1 is convergent_to_-infty ; :: thesis:

then seq1 is convergent by MESFUNC5:def 11;
then lim seq1 = -infty by A40, MESFUNC5:def 12;
hence lim seq1 <= lim seq2 by XXREAL_0:5; :: thesis:

end;

end;