let T1, T2 be TopSpace; :: thesis: for A2 being Subset of T2
for f being Function of T1,T2 st f is being_homeomorphism holds
f " A2,A2 are_homeomorphic
let A2 be Subset of T2; :: thesis: for f being Function of T1,T2 st f is being_homeomorphism holds
f " A2,A2 are_homeomorphic
let f be Function of T1,T2; :: thesis: ( f is being_homeomorphism implies f " A2,A2 are_homeomorphic )
assume A1: f is being_homeomorphism ; :: thesis: f " A2,A2 are_homeomorphic
A2: dom (A2 |` f) = f " A2 by Th1
.= [#] (T1 | (f " A2)) by PRE_TOPC:def 5 ;
rng f = [#] T2 by A1, TOPS_2:def 5;
then rng (A2 |` f) = A2 by RELAT_1:89
.= [#] (T2 | A2) by PRE_TOPC:def 5 ;
then reconsider g = A2 |` f as Function of (T1 | (f " A2)),(T2 | A2) by A2, FUNCT_2:1;
g is being_homeomorphism by A1, Th4;
hence f " A2,A2 are_homeomorphic by T_0TOPSP:def 1, METRIZTS:def 1; :: thesis: verum