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 3 :: thesis: ( X0 is closed implies (Inv f) " X0 is closed )
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: (Inv f) " X0 is closed

now :: thesis: for x being object holds
( ( 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) ) )

let x be object ; :: 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) )

A5: (Inv X) /\ (rng f) c= Cl ((Inv X) /\ (rng f)) by MEASURE6:58;
assume A6: x in (Inv X) /\ (rng f) ; :: thesis: x in (Cl ((Inv X) /\ (rng f))) /\ (rng f)
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: verum

end;

assume A7: x in (Cl ((Inv X) /\ (rng f))) /\ (rng f) ; :: thesis: x in (Inv X) /\ (rng f)
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: contradiction
A12: x in rng f by A7, XBOOLE_0:def 4;

now :: thesis: not lim seq <> 0

rng (seq ") c= X

proof

let y be object ; :: 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 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: verum

end;

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

now :: thesis: for n being Nat holds not seq . n = 0

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

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: verum

end;

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

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: for x being object holds
( ( x in (Inv f) " X0 implies x in (Inv f) " X ) & ( x in (Inv f) " X implies x in (Inv f) " X0 ) )

let x be object ; :: 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 A25: x in (Inv f) " X0 ; :: thesis: x in (Inv f) " X
then A26: (Inv f) . x in X0 by FUNCT_2:38;
reconsider xx = x as set by TARSKI:1;

now :: thesis: (Inv f) . x in X

assume not (Inv f) . x in X ; :: thesis: contradiction
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: verum

end;

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

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: verum

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: verum