let seq1, seq2 be ExtREAL_sequence; :: thesis:
assume A1: for n being Nat holds seq1 . n = - (seq2 . n) ; :: thesis:

now :: thesis:

let z be object ; :: thesis:
assume z in rng (inferior_realsequence seq2) ; :: thesis:
then consider n being object such that
A2: n in dom (inferior_realsequence seq2) and
A3: z = (inferior_realsequence seq2) . n by FUNCT_1:def 3;
reconsider n = n as Element of NAT by A2;
consider R2 being non empty Subset of ExtREAL such that
A4: R2 = { (seq2 . k) where k is Nat : n <= k } and
A5: z = inf R2 by A3, RINFSUP2:def 6;
reconsider z2 = z as Element of ExtREAL by A3, XXREAL_0:def 1;
set R1 = { (seq1 . k) where k is Nat : n <= k } ;
reconsider R1 = { (seq1 . k) where k is Nat : n <= k } as non empty Subset of ExtREAL by RINFSUP2:5;
set z1 = - z2;
A6: ex K1 being non empty Subset of ExtREAL st
( K1 = { (seq1 . k) where k is Nat : n <= k } & (superior_realsequence seq1) . n = sup K1 ) by RINFSUP2:def 7;

now :: thesis:

let x be object ; :: thesis:
assume x in R1 ; :: thesis:
then consider k being Nat such that
A7: x = seq1 . k and
A8: n <= k ;
reconsider x1 = x as Element of ExtREAL by A7;
- x1 = - (- (seq2 . k)) by A1, A7;
then - x1 in { (seq2 . k2) where k2 is Nat : n <= k2 } by A8;
then - (- x1) in - R2 by A4;
hence x in - R2 ; :: thesis:

end;

then A9: R1 c= - R2 by TARSKI:def 3;

now :: thesis:

let x be object ; :: thesis:
assume x in - R2 ; :: thesis:
then consider y being R_eal such that
A10: x = - y and
A11: y in R2 ;
consider k being Nat such that
A12: y = seq2 . k and
A13: n <= k by A4, A11;
seq1 . k = - (seq2 . k) by A1;
hence x in R1 by A10, A12, A13; :: thesis:

end;

then - R2 c= R1 by TARSKI:def 3;
then - R2 = R1 by A9, XBOOLE_0:def 10;
then (superior_realsequence seq1) . n = - z2 by A5, A6, SUPINF_2:15;
then A14: - z2 in rng (superior_realsequence seq1) by FUNCT_2:4;
z2 = - (- z2) ;
hence z in - (rng (superior_realsequence seq1)) by A14; :: thesis:

end;

then A15: rng (inferior_realsequence seq2) c= - (rng (superior_realsequence seq1)) by TARSKI:def 3;

now :: thesis:

let z be object ; :: thesis:
assume z in rng (superior_realsequence seq2) ; :: thesis:
then consider n being object such that
A16: n in dom (superior_realsequence seq2) and
A17: z = (superior_realsequence seq2) . n by FUNCT_1:def 3;
reconsider n = n as Element of NAT by A16;
consider R2 being non empty Subset of ExtREAL such that
A18: R2 = { (seq2 . k) where k is Nat : n <= k } and
A19: z = sup R2 by A17, RINFSUP2:def 7;
reconsider z2 = z as Element of ExtREAL by A17, XXREAL_0:def 1;
set R1 = { (seq1 . k) where k is Nat : n <= k } ;
reconsider R1 = { (seq1 . k) where k is Nat : n <= k } as non empty Subset of ExtREAL by RINFSUP2:5;
set z1 = - z2;
A20: ex K1 being non empty Subset of ExtREAL st
( K1 = { (seq1 . k) where k is Nat : n <= k } & (inferior_realsequence seq1) . n = inf K1 ) by RINFSUP2:def 6;

now :: thesis:

let x be object ; :: thesis:
assume x in R1 ; :: thesis:
then consider k being Nat such that
A21: x = seq1 . k and
A22: n <= k ;
reconsider x1 = x as Element of ExtREAL by A21;
- x1 = - (- (seq2 . k)) by A1, A21;
then - x1 in { (seq2 . k2) where k2 is Nat : n <= k2 } by A22;
then - (- x1) in - R2 by A18;
hence x in - R2 ; :: thesis:

end;

then A23: R1 c= - R2 by TARSKI:def 3;

now :: thesis:

let x be object ; :: thesis:
assume x in - R2 ; :: thesis:
then consider y being R_eal such that
A24: x = - y and
A25: y in R2 ;
consider k being Nat such that
A26: y = seq2 . k and
A27: n <= k by A18, A25;
seq1 . k = - (seq2 . k) by A1;
hence x in R1 by A24, A26, A27; :: thesis:

end;

then - R2 c= R1 by TARSKI:def 3;
then - R2 = R1 by A23, XBOOLE_0:def 10;
then (inferior_realsequence seq1) . n = - z2 by A19, A20, SUPINF_2:14;
then A28: - z2 in rng (inferior_realsequence seq1) by FUNCT_2:4;
z2 = - (- z2) ;
hence z in - (rng (inferior_realsequence seq1)) by A28; :: thesis:

end;

then A29: rng (superior_realsequence seq2) c= - (rng (inferior_realsequence seq1)) by TARSKI:def 3;

now :: thesis:

let z be object ; :: thesis:
assume z in - (rng (superior_realsequence seq1)) ; :: thesis:
then consider t being R_eal such that
A30: z = - t and
A31: t in rng (superior_realsequence seq1) ;
consider n being object such that
A32: n in dom (superior_realsequence seq1) and
A33: t = (superior_realsequence seq1) . n by A31, FUNCT_1:def 3;
reconsider n = n as Element of NAT by A32;
consider R1 being non empty Subset of ExtREAL such that
A34: R1 = { (seq1 . k) where k is Nat : n <= k } and
A35: t = sup R1 by A33, RINFSUP2:def 7;
reconsider z1 = z as Element of ExtREAL by A30;
set R2 = { (seq2 . k) where k is Nat : n <= k } ;
reconsider R2 = { (seq2 . k) where k is Nat : n <= k } as non empty Subset of ExtREAL by RINFSUP2:5;
A36: ex K2 being non empty Subset of ExtREAL st
( K2 = { (seq2 . k) where k is Nat : n <= k } & (inferior_realsequence seq2) . n = inf K2 ) by RINFSUP2:def 6;

now :: thesis:

let x be object ; :: thesis:
assume x in R2 ; :: thesis:
then consider k being Nat such that
A37: x = seq2 . k and
A38: n <= k ;
reconsider x1 = x as Element of ExtREAL by A37;
- x1 = - (- (seq1 . k)) by A1, A37;
then - x1 in { (seq1 . k2) where k2 is Nat : n <= k2 } by A38;
then - (- x1) in - R1 by A34;
hence x in - R1 ; :: thesis:

end;

then A39: R2 c= - R1 by TARSKI:def 3;

now :: thesis:

let x be object ; :: thesis:
assume x in - R1 ; :: thesis:
then consider y being R_eal such that
A40: x = - y and
A41: y in R1 ;
consider k being Nat such that
A42: y = seq1 . k and
A43: n <= k by A34, A41;
seq1 . k = - (seq2 . k) by A1;
hence x in R2 by A40, A42, A43; :: thesis:

end;

then - R1 c= R2 by TARSKI:def 3;
then - R1 = R2 by A39, XBOOLE_0:def 10;
then (inferior_realsequence seq2) . n = z1 by A30, A35, A36, SUPINF_2:14;
hence z in rng (inferior_realsequence seq2) by FUNCT_2:4; :: thesis:

end;

then - (rng (superior_realsequence seq1)) c= rng (inferior_realsequence seq2) by TARSKI:def 3;
then rng (inferior_realsequence seq2) = - (rng (superior_realsequence seq1)) by A15, XBOOLE_0:def 10;
hence lim_inf seq2 = - (lim_sup seq1) by SUPINF_2:15; :: thesis:

now :: thesis:

let z be object ; :: thesis:
assume z in - (rng (inferior_realsequence seq1)) ; :: thesis:
then consider t being R_eal such that
A44: z = - t and
A45: t in rng (inferior_realsequence seq1) ;
consider n being object such that
A46: n in dom (inferior_realsequence seq1) and
A47: t = (inferior_realsequence seq1) . n by A45, FUNCT_1:def 3;
reconsider n = n as Element of NAT by A46;
consider R1 being non empty Subset of ExtREAL such that
A48: R1 = { (seq1 . k) where k is Nat : n <= k } and
A49: t = inf R1 by A47, RINFSUP2:def 6;
reconsider z1 = z as Element of ExtREAL by A44;
set R2 = { (seq2 . k) where k is Nat : n <= k } ;
reconsider R2 = { (seq2 . k) where k is Nat : n <= k } as non empty Subset of ExtREAL by RINFSUP2:5;
A50: ex K2 being non empty Subset of ExtREAL st
( K2 = { (seq2 . k) where k is Nat : n <= k } & (superior_realsequence seq2) . n = sup K2 ) by RINFSUP2:def 7;

now :: thesis:

let x be object ; :: thesis:
assume x in R2 ; :: thesis:
then consider k being Nat such that
A51: x = seq2 . k and
A52: n <= k ;
reconsider x1 = x as Element of ExtREAL by A51;
seq1 . k = - (seq2 . k) by A1;
then - x1 in R1 by A48, A51, A52;
then - (- x1) in - R1 ;
hence x in - R1 ; :: thesis:

end;

then A53: R2 c= - R1 by TARSKI:def 3;

now :: thesis:

let x be object ; :: thesis:
assume x in - R1 ; :: thesis:
then consider y being R_eal such that
A54: x = - y and
A55: y in R1 ;
consider k being Nat such that
A56: y = seq1 . k and
A57: n <= k by A48, A55;
seq1 . k = - (seq2 . k) by A1;
hence x in R2 by A54, A56, A57; :: thesis:

end;

then - R1 c= R2 by TARSKI:def 3;
then - R1 = R2 by A53, XBOOLE_0:def 10;
then (superior_realsequence seq2) . n = z1 by A44, A49, A50, SUPINF_2:15;
hence z in rng (superior_realsequence seq2) by FUNCT_2:4; :: thesis:

end;

then - (rng (inferior_realsequence seq1)) c= rng (superior_realsequence seq2) by TARSKI:def 3;
then rng (superior_realsequence seq2) = - (rng (inferior_realsequence seq1)) by A29, XBOOLE_0:def 10;
hence lim_sup seq2 = - (lim_inf seq1) by SUPINF_2:14; :: thesis: