let r be positive real number ; :: 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: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