let n be Nat; :: thesis: for seq being ExtREAL_sequence holds

( (superior_realsequence seq) . n = sup (seq ^\ n) & (inferior_realsequence seq) . n = inf (seq ^\ n) )

let seq be ExtREAL_sequence; :: thesis: ( (superior_realsequence seq) . n = sup (seq ^\ n) & (inferior_realsequence seq) . n = inf (seq ^\ n) )

set rseq = seq ^\ n;

A1: ex Z being non empty Subset of ExtREAL st

( Z = { (seq . k) where k is Nat : n <= k } & (inferior_realsequence seq) . n = inf Z ) by Def6;

ex Y being non empty Subset of ExtREAL st

( Y = { (seq . k) where k is Nat : n <= k } & (superior_realsequence seq) . n = sup Y ) by Def7;

hence ( (superior_realsequence seq) . n = sup (seq ^\ n) & (inferior_realsequence seq) . n = inf (seq ^\ n) ) by A1, A4, A8, XBOOLE_0:def 10; :: thesis: verum

( (superior_realsequence seq) . n = sup (seq ^\ n) & (inferior_realsequence seq) . n = inf (seq ^\ n) )

let seq be ExtREAL_sequence; :: thesis: ( (superior_realsequence seq) . n = sup (seq ^\ n) & (inferior_realsequence seq) . n = inf (seq ^\ n) )

set rseq = seq ^\ n;

A1: ex Z being non empty Subset of ExtREAL st

( Z = { (seq . k) where k is Nat : n <= k } & (inferior_realsequence seq) . n = inf Z ) by Def6;

now :: thesis: for x being object st x in { (seq . k) where k is Nat : n <= k } holds

x in rng (seq ^\ n)

then A4:
{ (seq . k) where k is Nat : n <= k } c= rng (seq ^\ n)
;x in rng (seq ^\ n)

let x be object ; :: thesis: ( x in { (seq . k) where k is Nat : n <= k } implies x in rng (seq ^\ n) )

assume x in { (seq . k) where k is Nat : n <= k } ; :: thesis: x in rng (seq ^\ n)

then consider k being Nat such that

A2: x = seq . k and

A3: n <= k ;

reconsider k1 = k - n as Element of NAT by A3, INT_1:5;

x = seq . (n + k1) by A2;

then x = (seq ^\ n) . k1 by NAT_1:def 3;

hence x in rng (seq ^\ n) by FUNCT_2:4; :: thesis: verum

end;assume x in { (seq . k) where k is Nat : n <= k } ; :: thesis: x in rng (seq ^\ n)

then consider k being Nat such that

A2: x = seq . k and

A3: n <= k ;

reconsider k1 = k - n as Element of NAT by A3, INT_1:5;

x = seq . (n + k1) by A2;

then x = (seq ^\ n) . k1 by NAT_1:def 3;

hence x in rng (seq ^\ n) by FUNCT_2:4; :: thesis: verum

now :: thesis: for x being object st x in rng (seq ^\ n) holds

x in { (seq . k) where k is Nat : n <= k }

then A8:
rng (seq ^\ n) c= { (seq . k) where k is Nat : n <= k }
;x in { (seq . k) where k is Nat : n <= k }

let x be object ; :: thesis: ( x in rng (seq ^\ n) implies x in { (seq . k) where k is Nat : n <= k } )

assume x in rng (seq ^\ n) ; :: thesis: x in { (seq . k) where k is Nat : n <= k }

then consider z being object such that

A5: z in dom (seq ^\ n) and

A6: x = (seq ^\ n) . z by FUNCT_1:def 3;

reconsider k0 = z as Element of NAT by A5;

A7: n <= n + k0 by NAT_1:11;

x = seq . (n + k0) by A6, NAT_1:def 3;

hence x in { (seq . k) where k is Nat : n <= k } by A7; :: thesis: verum

end;assume x in rng (seq ^\ n) ; :: thesis: x in { (seq . k) where k is Nat : n <= k }

then consider z being object such that

A5: z in dom (seq ^\ n) and

A6: x = (seq ^\ n) . z by FUNCT_1:def 3;

reconsider k0 = z as Element of NAT by A5;

A7: n <= n + k0 by NAT_1:11;

x = seq . (n + k0) by A6, NAT_1:def 3;

hence x in { (seq . k) where k is Nat : n <= k } by A7; :: thesis: verum

ex Y being non empty Subset of ExtREAL st

( Y = { (seq . k) where k is Nat : n <= k } & (superior_realsequence seq) . n = sup Y ) by Def7;

hence ( (superior_realsequence seq) . n = sup (seq ^\ n) & (inferior_realsequence seq) . n = inf (seq ^\ n) ) by A1, A4, A8, XBOOLE_0:def 10; :: thesis: verum