let T, S, R be non empty TopSpace; :: thesis: for f being Function of T,S
for g being Function of S,T
for h being Function of S,R st f * g = id S & h is being_homeomorphism holds
(h * f) * (g * (h ")) = id R
let f be Function of T,S; :: thesis: for g being Function of S,T
for h being Function of S,R st f * g = id S & h is being_homeomorphism holds
(h * f) * (g * (h ")) = id R
let g be Function of S,T; :: thesis: for h being Function of S,R st f * g = id S & h is being_homeomorphism holds
(h * f) * (g * (h ")) = id R
let h be Function of S,R; :: thesis: ( f * g = id S & h is being_homeomorphism implies (h * f) * (g * (h ")) = id R )
assume that
A1: f * g = id S and
A2: h is being_homeomorphism ; :: thesis: (h * f) * (g * (h ")) = id R
A3: h is one-to-one by A2, TOPS_2:def 5;
A4: rng h = [#] R by A2, TOPS_2:def 5;
thus (h * f) * (g * (h ")) = ((h * f) * g) * (h ") by RELAT_1:36
.= (h * (id the carrier of S)) * (h ") by A1, RELAT_1:36
.= h * (h ") by FUNCT_2:17
.= id R by A3, A4, TOPS_2:52 ; :: thesis: verum