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

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