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: Cl A = [#] S by TOPS_1:def 3;
A3: rng f = [#] T by A1, TOPS_2:def 5;
thus Cl (f .: A) = f .: the carrier of S by A1, A2, TOPS_2:74
.= [#] T by A3, FUNCT_2:45 ; :: according to TOPS_1:def 3 :: thesis: verum