set f = Ciso ;

now

let x, y be Element of INT.Group ; :: thesis: 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 3;
reconsider tx = AffineMap 1,x as Function of R^1 ,R^1 by TOPMETR:24;
set p = tx * (ExtendInt y);
tx * (ExtendInt y) is Path of R^1 x, R^1 (x + y)

proof

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;
hence tx * (ExtendInt y) is continuous ; :: according to BORSUK_2:def 4 :: thesis: ( (tx * (ExtendInt y)) . 0 = R^1 x & (tx * (ExtendInt y)) . 1 = R^1 (x + y) )
thus (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 ; :: thesis: (tx * (ExtendInt y)) . 1 = R^1 (x + y)
thus (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 ; :: thesis: verum

end;

then reconsider p = tx * (ExtendInt y) as Path of R^1 x, R^1 (x + y) ;
Ciso . x = Class (EqRel (Tunit_circle 2),c[10] ),(cLoop x) by Def5;
then A4: fX, cLoop x are_homotopic by A1, TOPALG_1:47;
Ciso . y = Class (EqRel (Tunit_circle 2),c[10] ),(cLoop y) by Def5;
then fY, cLoop y are_homotopic by A2, TOPALG_1:47;
then A5: fX + fY,(cLoop x) + (cLoop y) are_homotopic by A4, BORSUK_6:84;
A6: for a being Point of I[01] holds (CircleMap * ((ExtendInt x) + p)) . a = ((cLoop x) + (cLoop y)) . a

proof

let a be Point of I[01] ; :: thesis: (CircleMap * ((ExtendInt x) + p)) . a = ((cLoop x) + (cLoop y)) . a

per cases ( a <= 1 / 2 or 1 / 2 <= a ) ;

suppose A7: a <= 1 / 2 ; :: thesis: (CircleMap * ((ExtendInt x) + p)) . a = ((cLoop x) + (cLoop y)) . a

then A8: 2 * a is Point of I[01] by BORSUK_6:6;
thus (CircleMap * ((ExtendInt x) + p)) . a = CircleMap . (((ExtendInt x) + p) . a) by FUNCT_2:21
.= CircleMap . ((ExtendInt x) . (2 * a)) by A7, BORSUK_6:def 4
.= CircleMap . (x * (2 * a)) by A8, Def1
.= |[(cos ((2 * PI ) * (x * (2 * a)))),(sin ((2 * PI ) * (x * (2 * a))))]| by TOPREALB:def 11
.= |[(cos (((2 * PI ) * x) * (2 * a))),(sin (((2 * PI ) * x) * (2 * a)))]|
.= (cLoop x) . (2 * a) by A8, Def4
.= ((cLoop x) + (cLoop y)) . a by A7, BORSUK_6:def 4 ; :: thesis: verum

end;

suppose A9: 1 / 2 <= a ; :: thesis: (CircleMap * ((ExtendInt x) + p)) . a = ((cLoop x) + (cLoop y)) . a

then A10: (2 * a) - 1 is Point of I[01] by BORSUK_6:7;
thus (CircleMap * ((ExtendInt x) + p)) . a = CircleMap . (((ExtendInt x) + p) . a) by FUNCT_2:21
.= CircleMap . (p . ((2 * a) - 1)) by A9, BORSUK_6:def 4
.= CircleMap . (tx . ((ExtendInt y) . ((2 * a) - 1))) by A10, FUNCT_2:21
.= CircleMap . (tx . (y * ((2 * a) - 1))) by A10, Def1
.= CircleMap . ((1 * (y * ((2 * a) - 1))) + x) by JORDAN16:def 3
.= |[(cos ((2 * PI ) * ((y * ((2 * a) - 1)) + x))),(sin ((2 * PI ) * ((y * ((2 * a) - 1)) + x)))]| by TOPREALB:def 11
.= |[(cos ((2 * PI ) * (y * ((2 * a) - 1)))),(sin (((2 * PI ) * (y * ((2 * a) - 1))) + ((2 * PI ) * x)))]| by COMPLEX2:10
.= |[(cos (((2 * PI ) * y) * ((2 * a) - 1))),(sin (((2 * PI ) * y) * ((2 * a) - 1)))]| by COMPLEX2:9
.= (cLoop y) . ((2 * a) - 1) by A10, Def4
.= ((cLoop x) + (cLoop y)) . a by A9, BORSUK_6:def 4 ; :: thesis: verum

end;

end;

end;

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 A6, FUNCT_2:113
.= (Ciso . x) * (Ciso . y) by A3, A5, TOPALG_1:47 ; :: thesis: verum

end;

hence Ciso is Homomorphism of INT.Group ,(pi_1 (Tunit_circle 2),c[10] ) by GROUP_6:def 7; :: thesis: verum