let X be non empty TopSpace; :: thesis: for x0, x1 being Point of st x0,x1 are_connected holds
pi_1 X,x0, pi_1 X,x1 are_isomorphic
let x0, x1 be Point of ; :: thesis: ( x0,x1 are_connected implies pi_1 X,x0, pi_1 X,x1 are_isomorphic )
consider P being Path of x1,x0;
assume A1: x0,x1 are_connected ; :: thesis: pi_1 X,x0, pi_1 X,x1 are_isomorphic
then reconsider h = pi_1-iso P as Homomorphism of pi_1 X,x0, pi_1 X,x1 by Th51;
take h ; :: according to GROUP_6:def 15 :: thesis: h is bijective
thus h is bijective by A1, Th56; :: thesis: verum