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;

take (pi_1-iso the Path of t,f . s) * (FundGrIso (f,s)) ; :: according to GROUP_6:def 11 :: thesis: (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; :: thesis: verum

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;

take (pi_1-iso the Path of t,f . s) * (FundGrIso (f,s)) ; :: according to GROUP_6:def 11 :: thesis: (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; :: thesis: verum