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

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