let r be positive real number ; :: thesis: for o being Point of
for x being Point of holds INT.Group , pi_1 (Tcircle o,r),x are_isomorphic
let o be Point of ; :: thesis: for x being Point of holds INT.Group , pi_1 (Tcircle o,r),x are_isomorphic
let x be Point of ; :: 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:35, 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 by GROUP_6:def 15;
take h * Ciso ; :: according to GROUP_6:def 15 :: thesis: h * Ciso is bijective
thus h * Ciso is bijective by A1, GROUP_6:74; :: thesis: verum