let X be without_zero Subset of REAL ; :: thesis: ( X is closed & X is bounded implies Inv X is closed )
assume that
A1: X is closed and
A2: X is bounded ; :: thesis: Inv X is closed
let s1 be Real_Sequence; :: according to RCOMP_1:def 4 :: thesis: ( not proj2 s1 c= Inv X or not s1 is convergent or lim s1 in Inv X )
assume that
A3: rng s1 c= Inv X and
A4: s1 is convergent ; :: thesis: lim s1 in Inv X
A5: not 0 in rng s1 by A3;

A6: now

assume not s1 is non-zero ; :: thesis: contradiction
then ex n being Element of NAT st s1 . n = 0 by SEQ_1:7;
hence contradiction by A5, FUNCT_2:6; :: thesis: verum

end;

A7: now

assume A8: lim s1 = 0 ; :: thesis: contradiction
A9: rng (s1 " ) c= X

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (s1 " ) or y in X )
assume y in rng (s1 " ) ; :: thesis: y in X
then consider x being set such that
A10: ( x in dom (s1 " ) & y = (s1 " ) . x ) by FUNCT_1:def 5;
reconsider x = x as Element of NAT by A10;
A11: (s1 " ) . x = (s1 . x) " by VALUED_1:10;
s1 . x in rng s1 by FUNCT_2:6;
then 1 / (s1 . x) in Inv (Inv X) by A3;
hence y in X by A10, A11; :: thesis: verum

end;

not s1 " is bounded by A4, A6, A8, Th6;
then not rng (s1 " ) is bounded by Th7;
hence contradiction by A2, A9, XXREAL_2:45; :: thesis: verum

end;

then A12: s1 " is convergent by A4, A6, SEQ_2:35;
rng (s1 " ) c= X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (s1 " ) or x in X )
assume x in rng (s1 " ) ; :: thesis: x in X
then consider n being set such that
A13: n in dom (s1 " ) and
A14: x = (s1 " ) . n by FUNCT_1:def 5;
reconsider n = n as Element of NAT by A13;
A15: x = (s1 . n) " by A14, VALUED_1:10;
s1 . n in rng s1 by FUNCT_2:6;
then 1 / (s1 . n) in Inv (Inv X) by A3;
hence x in X by A15; :: thesis: verum

end;

then A16: lim (s1 " ) in X by A1, A12, RCOMP_1:def 4;
(lim s1) " = lim (s1 " ) by A4, A6, A7, SEQ_2:36;
then 1 / (lim s1) in X by A16;
then 1 / (1 / (lim s1)) in Inv X ;
hence lim s1 in Inv X ; :: thesis: verum