let seq1, seq2 be ExtREAL_sequence; :: thesis: ( ( for n being Nat holds seq1 . n = - (seq2 . n) ) implies ( lim_inf seq2 = - (lim_sup seq1) & lim_sup seq2 = - (lim_inf seq1) ) )
assume A0: for n being Nat holds seq1 . n = - (seq2 . n) ; :: thesis: ( lim_inf seq2 = - (lim_sup seq1) & lim_sup seq2 = - (lim_inf seq1) )

now

let z be set ; :: thesis: ( z in rng (inferior_realsequence seq2) implies z in - (rng (superior_realsequence seq1)) )
assume z in rng (inferior_realsequence seq2) ; :: thesis: z in - (rng (superior_realsequence seq1))
then consider n being set such that
A21: ( n in dom (inferior_realsequence seq2) & z = (inferior_realsequence seq2) . n ) by FUNCT_1:def 5;
reconsider z2 = z as Element of ExtREAL by A21;
reconsider n = n as Element of NAT by A21;
consider R2 being non empty Subset of ExtREAL such that
A22: ( R2 = { (seq2 . k) where k is Element of NAT : n <= k } & z = inf R2 ) by A21, RINFSUP2:def 6;
set R1 = { (seq1 . k) where k is Element of NAT : n <= k } ;
reconsider R1 = { (seq1 . k) where k is Element of NAT : n <= k } as non empty Subset of ExtREAL by RINFSUP2:5;
set z1 = - z2;
A25: z2 = - (- z2) ;

now

let x be set ; :: thesis: ( x in - R2 implies x in R1 )
assume x in - R2 ; :: thesis: x in R1
then consider y being R_eal such that
P01: ( y in R2 & x = - y ) by SUPINF_2:def 6;
consider k being Element of NAT such that
P02: ( y = seq2 . k & n <= k ) by P01, A22;
seq1 . k = - (seq2 . k) by A0;
hence x in R1 by P01, P02; :: thesis: verum

end;

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

now

let x be set ; :: thesis: ( x in R1 implies x in - R2 )
assume x in R1 ; :: thesis: x in - R2
then consider k being Element of NAT such that
P01: ( x = seq1 . k & n <= k ) ;
reconsider x1 = x as Element of ExtREAL by P01;
- x1 = - (- (seq2 . k)) by A0, P01;
then - x1 in { (seq2 . k2) where k2 is Element of NAT : n <= k2 } by P01;
then - (- x1) in - R2 by A22, SUPINF_2:23;
hence x in - R2 ; :: thesis: verum

end;

then R1 c= - R2 by TARSKI:def 3;
then A23: - R2 = R1 by R01, XBOOLE_0:def 10;
ex K1 being non empty Subset of ExtREAL st
( K1 = { (seq1 . k) where k is Element of NAT : n <= k } & (superior_realsequence seq1) . n = sup K1 ) by RINFSUP2:def 7;
then (superior_realsequence seq1) . n = - z2 by A22, A23, SUPINF_2:33;
then - z2 in rng (superior_realsequence seq1) by FUNCT_2:6;
hence z in - (rng (superior_realsequence seq1)) by A25, SUPINF_2:def 6; :: thesis: verum

end;

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

now

let z be set ; :: thesis: ( z in - (rng (superior_realsequence seq1)) implies z in rng (inferior_realsequence seq2) )
assume z in - (rng (superior_realsequence seq1)) ; :: thesis: z in rng (inferior_realsequence seq2)
then consider t being R_eal such that
B20: ( t in rng (superior_realsequence seq1) & z = - t ) by SUPINF_2:def 6;
consider n being set such that
B21: ( n in dom (superior_realsequence seq1) & t = (superior_realsequence seq1) . n ) by B20, FUNCT_1:def 5;
reconsider z1 = z as Element of ExtREAL by B20;
reconsider n = n as Element of NAT by B21;
consider R1 being non empty Subset of ExtREAL such that
B22: ( R1 = { (seq1 . k) where k is Element of NAT : n <= k } & t = sup R1 ) by B21, RINFSUP2:def 7;
set R2 = { (seq2 . k) where k is Element of NAT : n <= k } ;
reconsider R2 = { (seq2 . k) where k is Element of NAT : n <= k } as non empty Subset of ExtREAL by RINFSUP2:5;

now

let x be set ; :: thesis: ( x in - R1 implies x in R2 )
assume x in - R1 ; :: thesis: x in R2
then consider y being R_eal such that
P01: ( y in R1 & x = - y ) by SUPINF_2:def 6;
consider k being Element of NAT such that
P02: ( y = seq1 . k & n <= k ) by P01, B22;
seq1 . k = - (seq2 . k) by A0;
hence x in R2 by P01, P02; :: thesis: verum

end;

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

now

let x be set ; :: thesis: ( x in R2 implies x in - R1 )
assume x in R2 ; :: thesis: x in - R1
then consider k being Element of NAT such that
P01: ( x = seq2 . k & n <= k ) ;
reconsider x1 = x as Element of ExtREAL by P01;
- x1 = - (- (seq1 . k)) by A0, P01;
then - x1 in { (seq1 . k2) where k2 is Element of NAT : n <= k2 } by P01;
then - (- x1) in - R1 by B22, SUPINF_2:23;
hence x in - R1 ; :: thesis: verum

end;

then R2 c= - R1 by TARSKI:def 3;
then B23: - R1 = R2 by R02, XBOOLE_0:def 10;
ex K2 being non empty Subset of ExtREAL st
( K2 = { (seq2 . k) where k is Element of NAT : n <= k } & (inferior_realsequence seq2) . n = inf K2 ) by RINFSUP2:def 6;
then (inferior_realsequence seq2) . n = z1 by B23, B20, B22, SUPINF_2:32;
hence z in rng (inferior_realsequence seq2) by FUNCT_2:6; :: thesis: verum

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 A26, XBOOLE_0:def 10;
hence lim_inf seq2 = - (lim_sup seq1) by SUPINF_2:33; :: thesis: lim_sup seq2 = - (lim_inf seq1)

now

let z be set ; :: thesis: ( z in rng (superior_realsequence seq2) implies z in - (rng (inferior_realsequence seq1)) )
assume z in rng (superior_realsequence seq2) ; :: thesis: z in - (rng (inferior_realsequence seq1))
then consider n being set such that
A31: ( n in dom (superior_realsequence seq2) & z = (superior_realsequence seq2) . n ) by FUNCT_1:def 5;
reconsider z2 = z as Element of ExtREAL by A31;
reconsider n = n as Element of NAT by A31;
consider R2 being non empty Subset of ExtREAL such that
A32: ( R2 = { (seq2 . k) where k is Element of NAT : n <= k } & z = sup R2 ) by A31, RINFSUP2:def 7;
set R1 = { (seq1 . k) where k is Element of NAT : n <= k } ;
reconsider R1 = { (seq1 . k) where k is Element of NAT : n <= k } as non empty Subset of ExtREAL by RINFSUP2:5;
set z1 = - z2;
A35: z2 = - (- z2) ;

now

let x be set ; :: thesis: ( x in - R2 implies x in R1 )
assume x in - R2 ; :: thesis: x in R1
then consider y being R_eal such that
P01: ( y in R2 & x = - y ) by SUPINF_2:def 6;
consider k being Element of NAT such that
P02: ( y = seq2 . k & n <= k ) by P01, A32;
seq1 . k = - (seq2 . k) by A0;
hence x in R1 by P01, P02; :: thesis: verum

end;

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

now

let x be set ; :: thesis: ( x in R1 implies x in - R2 )
assume x in R1 ; :: thesis: x in - R2
then consider k being Element of NAT such that
P01: ( x = seq1 . k & n <= k ) ;
reconsider x1 = x as Element of ExtREAL by P01;
- x1 = - (- (seq2 . k)) by P01, A0;
then - x1 in { (seq2 . k2) where k2 is Element of NAT : n <= k2 } by P01;
then - (- x1) in - R2 by A32, SUPINF_2:23;
hence x in - R2 ; :: thesis: verum

end;

then R1 c= - R2 by TARSKI:def 3;
then A33: - R2 = R1 by R01, XBOOLE_0:def 10;
ex K1 being non empty Subset of ExtREAL st
( K1 = { (seq1 . k) where k is Element of NAT : n <= k } & (inferior_realsequence seq1) . n = inf K1 ) by RINFSUP2:def 6;
then (inferior_realsequence seq1) . n = - z2 by A32, A33, SUPINF_2:32;
then - z2 in rng (inferior_realsequence seq1) by FUNCT_2:6;
hence z in - (rng (inferior_realsequence seq1)) by A35, SUPINF_2:def 6; :: thesis: verum

end;

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

now

let z be set ; :: thesis: ( z in - (rng (inferior_realsequence seq1)) implies z in rng (superior_realsequence seq2) )
assume z in - (rng (inferior_realsequence seq1)) ; :: thesis: z in rng (superior_realsequence seq2)
then consider t being R_eal such that
B30: ( t in rng (inferior_realsequence seq1) & z = - t ) by SUPINF_2:def 6;
consider n being set such that
B31: ( n in dom (inferior_realsequence seq1) & t = (inferior_realsequence seq1) . n ) by B30, FUNCT_1:def 5;
reconsider z1 = z as Element of ExtREAL by B30;
reconsider n = n as Element of NAT by B31;
consider R1 being non empty Subset of ExtREAL such that
B32: ( R1 = { (seq1 . k) where k is Element of NAT : n <= k } & t = inf R1 ) by B31, RINFSUP2:def 6;
set R2 = { (seq2 . k) where k is Element of NAT : n <= k } ;
reconsider R2 = { (seq2 . k) where k is Element of NAT : n <= k } as non empty Subset of ExtREAL by RINFSUP2:5;

now

let x be set ; :: thesis: ( x in - R1 implies x in R2 )
assume x in - R1 ; :: thesis: x in R2
then consider y being R_eal such that
P01: ( y in R1 & x = - y ) by SUPINF_2:def 6;
consider k being Element of NAT such that
P02: ( y = seq1 . k & n <= k ) by P01, B32;
seq1 . k = - (seq2 . k) by A0;
hence x in R2 by P01, P02; :: thesis: verum

end;

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

now

let x be set ; :: thesis: ( x in R2 implies x in - R1 )
assume x in R2 ; :: thesis: x in - R1
then consider k being Element of NAT such that
P01: ( x = seq2 . k & n <= k ) ;
reconsider x1 = x as Element of ExtREAL by P01;
seq1 . k = - (seq2 . k) by A0;
then - x1 in R1 by P01, B32;
then - (- x1) in - R1 by SUPINF_2:23;
hence x in - R1 ; :: thesis: verum

end;

then R2 c= - R1 by TARSKI:def 3;
then B33: - R1 = R2 by R02, XBOOLE_0:def 10;
ex K2 being non empty Subset of ExtREAL st
( K2 = { (seq2 . k) where k is Element of NAT : n <= k } & (superior_realsequence seq2) . n = sup K2 ) by RINFSUP2:def 7;
then (superior_realsequence seq2) . n = z1 by B33, B30, B32, SUPINF_2:33;
hence z in rng (superior_realsequence seq2) by FUNCT_2:6; :: thesis: verum

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 A36, XBOOLE_0:def 10;
hence lim_sup seq2 = - (lim_inf seq1) by SUPINF_2:32; :: thesis: verum