let T be TopStruct ; :: thesis: for f being RealMap of T st f is continuous & not 0 in rng f holds
Inv f is continuous
let f be RealMap of T; :: thesis: ( f is continuous & not 0 in rng f implies Inv f is continuous )
assume that
A1: f is continuous and
A2: not 0 in rng f ; :: thesis: Inv f is continuous
let X0 be Subset of REAL ; :: according to PSCOMP_1:def 25 :: thesis: ( X0 is closed implies (Inv f) " X0 is closed )
assume A3: X0 is closed ; :: thesis: (Inv f) " X0 is closed
0 in {0 } by TARSKI:def 1;
then A4: not 0 in X0 \ {0 } by XBOOLE_0:def 5;
A5: X0 \ {0 } c= X0 by XBOOLE_1:36;
reconsider X = X0 \ {0 } as without_zero Subset of REAL by A4, Def1;
set X' = Inv X;
set X'r = (Inv X) /\ (rng f);

now

let x be set ; :: thesis: ( ( x in (Inv X) /\ (rng f) implies x in (Cl ((Inv X) /\ (rng f))) /\ (rng f) ) & ( x in (Cl ((Inv X) /\ (rng f))) /\ (rng f) implies x in (Inv X) /\ (rng f) ) )

hereby :: thesis: ( x in (Cl ((Inv X) /\ (rng f))) /\ (rng f) implies x in (Inv X) /\ (rng f) )

assume A6: x in (Inv X) /\ (rng f) ; :: thesis: x in (Cl ((Inv X) /\ (rng f))) /\ (rng f)
(Inv X) /\ (rng f) c= Cl ((Inv X) /\ (rng f)) by Th33;
then ( x in Cl ((Inv X) /\ (rng f)) & x in rng f ) by A6, XBOOLE_0:def 4;
hence x in (Cl ((Inv X) /\ (rng f))) /\ (rng f) by XBOOLE_0:def 4; :: thesis: verum

end;

assume A7: x in (Cl ((Inv X) /\ (rng f))) /\ (rng f) ; :: thesis: x in (Inv X) /\ (rng f)
then A8: ( x in Cl ((Inv X) /\ (rng f)) & x in rng f ) by XBOOLE_0:def 4;
reconsider s = x as Real by A7;
consider seq being Real_Sequence such that
A9: rng seq c= (Inv X) /\ (rng f) and
A10: seq is convergent and
A11: lim seq = s by A8, Th39;
assume not x in (Inv X) /\ (rng f) ; :: thesis: contradiction
then A12: not x in Inv X by A8, XBOOLE_0:def 4;

now

assume A13: lim seq <> 0 ; :: thesis: contradiction

now

let n be Element of NAT ; :: thesis: not seq . n = 0
assume seq . n = 0 ; :: thesis: contradiction
then 0 in rng seq by FUNCT_2:6;
hence contradiction by A2, A9, XBOOLE_0:def 4; :: thesis: verum

end;

then A14: seq is non-zero by SEQ_1:7;
then A15: seq " is convergent by A10, A13, SEQ_2:35;
A16: lim (seq " ) = (lim seq) " by A10, A13, A14, SEQ_2:36;
rng (seq " ) c= X

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (seq " ) or y in X )
assume y in rng (seq " ) ; :: thesis: y in X
then consider n being set such that
A17: ( n in dom (seq " ) & y = (seq " ) . n ) by FUNCT_1:def 5;
reconsider n = n as Element of NAT by A17;
seq . n in rng seq by FUNCT_2:6;
then seq . n in Inv X by A9, XBOOLE_0:def 4;
then A18: 1 / (1 / (seq . n)) in Inv X ;
(seq " ) . n = (seq . n) " by VALUED_1:10
.= 1 / (seq . n) ;
hence y in X by A17, A18, Th28; :: thesis: verum

end;

then rng (seq " ) c= X0 by A5, XBOOLE_1:1;
then A19: lim (seq " ) in X0 by A3, A15, RCOMP_1:def 4;
lim (seq " ) <> 0 by A13, A16, XCMPLX_1:203;
then not lim (seq " ) in {0 } by TARSKI:def 1;
then lim (seq " ) in X by A19, XBOOLE_0:def 5;
then 1 / (lim (seq " )) in Inv X ;
hence contradiction by A11, A12, A16; :: thesis: verum

end;

hence contradiction by A2, A7, A11, XBOOLE_0:def 4; :: thesis: verum

end;

then A20: (Inv X) /\ (rng f) = (Cl ((Inv X) /\ (rng f))) /\ (rng f) by TARSKI:2;
f " (Cl ((Inv X) /\ (rng f))) is closed by A1, Def25;
then A21: f " ((Inv X) /\ (rng f)) is closed by A20, RELAT_1:168;
A22: f " (Inv X) = f " ((Inv X) /\ (rng f)) by RELAT_1:168;
A23: (Inv f) " X = f " (Inv X) by Th46;

now

let x be set ; :: thesis: ( ( x in (Inv f) " X0 implies x in (Inv f) " X ) & ( x in (Inv f) " X implies x in (Inv f) " X0 ) )

hereby :: thesis: ( x in (Inv f) " X implies x in (Inv f) " X0 )

assume A24: x in (Inv f) " X0 ; :: thesis: x in (Inv f) " X
then A25: ( x in the carrier of T & (Inv f) . x in X0 ) by FUNCT_2:46;

now

assume not (Inv f) . x in X ; :: thesis: contradiction
then (Inv f) . x in {0 } by A25, XBOOLE_0:def 5;
then (Inv f) . x = 0 by TARSKI:def 1;
then 0 = (f . x) " by VALUED_1:10;
hence contradiction by A2, A24, FUNCT_2:6, XCMPLX_1:203; :: thesis: verum

end;

hence x in (Inv f) " X by A24, FUNCT_2:46; :: thesis: verum

end;

(Inv f) " X c= (Inv f) " X0 by RELAT_1:178, XBOOLE_1:36;
hence ( x in (Inv f) " X implies x in (Inv f) " X0 ) ; :: thesis: verum

end;

hence (Inv f) " X0 is closed by A21, A22, A23, TARSKI:2; :: thesis: verum