let T1, T2 be TopSpace; :: thesis: for A1 being Subset of T1
for f being Function of T1,T2 st f is being_homeomorphism holds
A1,f .: A1 are_homeomorphic
let A1 be Subset of T1; :: thesis: for f being Function of T1,T2 st f is being_homeomorphism holds
A1,f .: A1 are_homeomorphic
let f be Function of T1,T2; :: thesis: ( f is being_homeomorphism implies A1,f .: A1 are_homeomorphic )
assume A1: f is being_homeomorphism ; :: thesis: A1,f .: A1 are_homeomorphic
dom f = [#] T1 by A1;
then A2: dom (f | A1) = ([#] T1) /\ A1 by RELAT_1:61
.= A1 by XBOOLE_1:28
.= [#] (T1 | A1) by PRE_TOPC:def 5 ;
rng (f | A1) = f .: A1 by RELAT_1:115
.= [#] (T2 | (f .: A1)) by PRE_TOPC:def 5 ;
then reconsider g = f | A1 as Function of (T1 | A1),(T2 | (f .: A1)) by A2, FUNCT_2:1;
g is being_homeomorphism by A1, Th2;
then T1 | A1,T2 | (f .: A1) are_homeomorphic by T_0TOPSP:def 1;
hence A1,f .: A1 are_homeomorphic ; :: thesis: verum