let S, T be non empty TopSpace; :: thesis: for f being Function of S,T
for A being dense Subset of S st f is being_homeomorphism holds
f .: A is dense
let f be Function of S,T; :: thesis: for A being dense Subset of S st f is being_homeomorphism holds
f .: A is dense
let A be dense Subset of S; :: thesis: ( f is being_homeomorphism implies f .: A is dense )
assume A1: f is being_homeomorphism ; :: thesis: f .: A is dense
A2: rng f = [#] T by A1, TOPS_2:def 5;
Cl A = [#] S by TOPS_1:def 3;
hence Cl (f .: A) = f .: the carrier of S by A1, TOPS_2:60
.= [#] T by A2, FUNCT_2:37 ;
:: according to TOPS_1:def 3 :: thesis: verum