let S, T be non empty TopSpace; :: thesis: for f being Function of S,T
for A being dense Subset of T st f is being_homeomorphism holds
f " A is dense
let f be Function of S,T; :: thesis: for A being dense Subset of T st f is being_homeomorphism holds
f " A is dense
let A be dense Subset of T; :: thesis: ( f is being_homeomorphism implies f " A is dense )
assume A1: f is being_homeomorphism ; :: thesis: f " A is dense
A2: Cl A = [#] T by TOPS_1:def 3;
thus Cl (f " A) = f " (Cl A) by A1, TOPS_2:59
.= [#] S by A2, TOPS_2:41 ; :: according to TOPS_1:def 3 :: thesis: verum