let S be non empty TopSpace; for T being non empty pathwise_connected TopSpace
for s being Point of S
for t being Point of T st S,T are_homeomorphic holds
pi_1 (S,s), pi_1 (T,t) are_isomorphic
let T be non empty pathwise_connected TopSpace; for s being Point of S
for t being Point of T st S,T are_homeomorphic holds
pi_1 (S,s), pi_1 (T,t) are_isomorphic
let s be Point of S; for t being Point of T st S,T are_homeomorphic holds
pi_1 (S,s), pi_1 (T,t) are_isomorphic
let t be Point of T; ( S,T are_homeomorphic implies pi_1 (S,s), pi_1 (T,t) are_isomorphic )
given f being Function of S,T such that A1:
f is being_homeomorphism
; T_0TOPSP:def 1 pi_1 (S,s), pi_1 (T,t) are_isomorphic
reconsider f = f as continuous Function of S,T by A1;
take
(pi_1-iso the Path of t,f . s) * (FundGrIso (f,s))
; GROUP_6:def 11 (pi_1-iso the Path of t,f . s) * (FundGrIso (f,s)) is bijective
FundGrIso (f,s) is bijective
by A1, Th31;
hence
(pi_1-iso the Path of t,f . s) * (FundGrIso (f,s)) is bijective
by GROUP_6:64; verum