set f = Ciso ;
now let x,
y be
Element of
INT.Group ;
Ciso . (x * y) = (Ciso . x) * (Ciso . y)consider fX,
fY being
Loop of
c[10] such that A1:
Ciso . x = Class (EqRel (Tunit_circle 2),c[10] ),
fX
and A2:
Ciso . y = Class (EqRel (Tunit_circle 2),c[10] ),
fY
and A3:
the
multF of
(pi_1 (Tunit_circle 2),c[10] ) . (Ciso . x),
(Ciso . y) = Class (EqRel (Tunit_circle 2),c[10] ),
(fX + fY)
by TOPALG_1:def 5;
Ciso . y = Class (EqRel (Tunit_circle 2),c[10] ),
(cLoop y)
by Def5;
then A4:
fY,
cLoop y are_homotopic
by A2, TOPALG_1:47;
reconsider tx =
AffineMap 1,
x as
Function of
R^1 ,
R^1 by TOPMETR:24;
set p =
tx * (ExtendInt y);
A5:
(tx * (ExtendInt y)) . 0 =
tx . ((ExtendInt y) . j0)
by FUNCT_2:21
.=
tx . (y * j0)
by Def1
.=
(1 * 0 ) + x
by JORDAN16:def 3
.=
R^1 x
by TOPREALB:def 2
;
A6:
(tx * (ExtendInt y)) . 1 =
tx . ((ExtendInt y) . j1)
by FUNCT_2:21
.=
tx . (y * j1)
by Def1
.=
(1 * y) + x
by JORDAN16:def 3
.=
R^1 (x + y)
by TOPREALB:def 2
;
x is
Real
by XREAL_0:def 1;
then
tx is
being_homeomorphism
by JORDAN16:35;
then
tx is
continuous
by TOPS_2:def 5;
then reconsider p =
tx * (ExtendInt y) as
Path of
R^1 x,
R^1 (x + y) by A5, A6, BORSUK_2:def 4;
A7:
for
a being
Point of
I[01] holds
(CircleMap * ((ExtendInt x) + p)) . a = ((cLoop x) + (cLoop y)) . a
Ciso . x = Class (EqRel (Tunit_circle 2),c[10] ),
(cLoop x)
by Def5;
then
fX,
cLoop x are_homotopic
by A1, TOPALG_1:47;
then A12:
fX + fY,
(cLoop x) + (cLoop y) are_homotopic
by A4, BORSUK_6:84;
thus Ciso . (x * y) =
Class (EqRel (Tunit_circle 2),c[10] ),
(CircleMap * ((ExtendInt x) + p))
by Th25
.=
Class (EqRel (Tunit_circle 2),c[10] ),
((cLoop x) + (cLoop y))
by A7, FUNCT_2:113
.=
(Ciso . x) * (Ciso . y)
by A3, A12, TOPALG_1:47
;
verum end;
hence
Ciso is Homomorphism of INT.Group ,(pi_1 (Tunit_circle 2),c[10] )
by GROUP_6:def 7; verum