let S be non empty TopSpace; :: thesis: 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; :: 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