let T be TopStruct ; :: thesis:
let f be RealMap of T; :: thesis:
assume that
A1: f is continuous and
A2: not 0 in rng f ; :: thesis:
let X0 be Subset of REAL; :: according to PSCOMP_1:def 3 :: thesis:
0 in {0} by TARSKI:def 1;
then not 0 in X0 \ {0} by XBOOLE_0:def 5;
then reconsider X = X0 \ {0} as without_zero Subset of REAL by MEASURE6:def 2;
set X9 = Inv X;
A3: X0 \ {0} c= X0 by XBOOLE_1:36;
set X9r = (Inv X) /\ (rng f);
assume A4: X0 is closed ; :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

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

end;

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

rng (seq ") c= X

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng (seq ") ; :: thesis:
then consider n being object such that
A13: n in dom (seq ") and
A14: y = (seq ") . n by FUNCT_1:def 3;
reconsider n = n as Element of NAT by A13;
seq . n in rng seq by FUNCT_2:4;
then A15: 1 / (1 / (seq . n)) in Inv X by A8, XBOOLE_0:def 4;
(seq ") . n = (seq . n) " by VALUED_1:10
.= 1 / (seq . n) ;
hence y in X by A14, A15, MEASURE6:54; :: thesis:

end;

then A16: rng (seq ") c= X0 by A3;
assume A17: lim seq <> 0 ; :: thesis:

let n be Nat; :: thesis:
A18: n in NAT by ORDINAL1:def 12;
assume seq . n = 0 ; :: thesis:
then 0 in rng seq by FUNCT_2:4, A18;
hence contradiction by A2, A8, XBOOLE_0:def 4; :: thesis:

end;

then A19: seq is non-zero by SEQ_1:5;
then seq " is convergent by A9, A17, SEQ_2:21;
then A20: lim (seq ") in X0 by A4, A16;
A21: lim (seq ") = (lim seq) " by A9, A17, A19, SEQ_2:22;
then lim (seq ") <> 0 by A17;
then not lim (seq ") in {0} by TARSKI:def 1;
then lim (seq ") in X by A20, XBOOLE_0:def 5;
then 1 / (lim (seq ")) in Inv X ;
hence contradiction by A12, A10, A11, A21, XBOOLE_0:def 4; :: thesis:

end;

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

end;

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

A24: now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume A25: x in (Inv f) " X0 ; :: thesis:
then A26: (Inv f) . x in X0 by FUNCT_2:38;
reconsider xx = x as set by TARSKI:1;

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

end;

hence x in (Inv f) " X by A25, FUNCT_2:38; :: thesis:

end;

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

end;

( f " (Inv X) = f " ((Inv X) /\ (rng f)) & (Inv f) " X = f " (Inv X) ) by MEASURE6:71, RELAT_1:133;
hence (Inv f) " X0 is closed by A23, A24, TARSKI:2; :: thesis: