let T be non empty arcwise_connected TopSpace; :: thesis: for y0, y1 being Point of T holds pi_1 T,y0, pi_1 T,y1 are_isomorphic
let y0, y1 be Point of T; :: thesis: pi_1 T,y0, pi_1 T,y1 are_isomorphic
consider R being Path of y1,y0;
take pi_1-iso R ; :: according to GROUP_6:def 15 :: thesis: pi_1-iso R is bijective
thus pi_1-iso R is bijective ; :: thesis: verum