let r be positive Real; :: thesis: for o being Point of (TOP-REAL 2)
for x being Point of (Tcircle (o,r)) holds INT.Group , pi_1 ((Tcircle (o,r)),x) are_isomorphic
let o be Point of (TOP-REAL 2); :: thesis: for x being Point of (Tcircle (o,r)) holds INT.Group , pi_1 ((Tcircle (o,r)),x) are_isomorphic
let x be Point of (Tcircle (o,r)); :: thesis: INT.Group , pi_1 ((Tcircle (o,r)),x) are_isomorphic
Tunit_circle 2 = Tcircle ((0. (TOP-REAL 2)),1) by TOPREALB:def 7;
then pi_1 ((Tunit_circle 2),c[10]), pi_1 ((Tcircle (o,r)),x) are_isomorphic by TOPALG_3:33, TOPREALB:20;
then consider h being Homomorphism of (pi_1 ((Tunit_circle 2),c[10])),(pi_1 ((Tcircle (o,r)),x)) such that
A1: h is bijective ;
take h * Ciso ; :: according to GROUP_6:def 11 :: thesis: h * Ciso is bijective
thus h * Ciso is bijective by A1, GROUP_6:64; :: thesis: verum