for T1, T2 being TopSpace
for A2 being Subset of T2
for f being Function of T1,T2 st f is being_homeomorphism holds
for g being Function of (T1 | (f " A2)),(T2 | A2) st g = A2 |` f holds
g is being_homeomorphism