let S be non empty TopSpace; :: thesis: for T being non empty arcwise_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 arcwise_connected TopSpace; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: according to T_0TOPSP:def 1 :: thesis: pi_1 S,s, pi_1 T,t are_isomorphic
reconsider f = f as continuous Function of S,T by A1, TOPS_2:def 5;
consider P being Path of t,f . s;
take (pi_1-iso P) * (FundGrIso f,s) ; :: according to GROUP_6:def 15 :: thesis: (pi_1-iso P) * (FundGrIso f,s) is bijective
FundGrIso f,s is bijective by A1, Th33;
hence (pi_1-iso P) * (FundGrIso f,s) is bijective by GROUP_6:74; :: thesis: verum