set f = Ciso ;
let x, y be Element of INT.Group; :: according to GROUP_6:def 6 :: 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 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:46;
reconsider tx = AffineMap (1,x) as Function of R^1,R^1 by TOPMETR:17;
set p = tx * (ExtendInt y);
A5: (tx * (ExtendInt y)) . 0 = tx . ((ExtendInt y) . j0) by FUNCT_2:15
.= tx . (y * j0) by Def1
.= (1 * 0) + x by FCONT_1:def 4
.= R^1 x by TOPREALB:def 2 ;
A6: (tx * (ExtendInt y)) . 1 = tx . ((ExtendInt y) . j1) by FUNCT_2:15
.= tx . (y * j1) by Def1
.= (1 * y) + x by FCONT_1:def 4
.= R^1 (x + y) by TOPREALB:def 2 ;
tx is being_homeomorphism by JORDAN16:20;
then tx is continuous ;
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

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 A8: a <= 1 / 2 ; :: thesis: (CircleMap * ((ExtendInt x) + p)) . a = ((cLoop x) + (cLoop y)) . a

then A9: 2 * a is Point of I[01] by BORSUK_6:3;
thus (CircleMap * ((ExtendInt x) + p)) . a = CircleMap . (((ExtendInt x) + p) . a) by FUNCT_2:15
.= CircleMap . ((ExtendInt x) . (2 * a)) by A8, BORSUK_6:def 2
.= CircleMap . (x * (2 * a)) by A9, 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 A9, Def4
.= ((cLoop x) + (cLoop y)) . a by A8, BORSUK_6:def 2 ; :: thesis: verum

end;

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

then A11: (2 * a) - 1 is Point of I[01] by BORSUK_6:4;
thus (CircleMap * ((ExtendInt x) + p)) . a = CircleMap . (((ExtendInt x) + p) . a) by FUNCT_2:15
.= CircleMap . (p . ((2 * a) - 1)) by A10, BORSUK_6:def 2
.= CircleMap . (tx . ((ExtendInt y) . ((2 * a) - 1))) by A11, FUNCT_2:15
.= CircleMap . (tx . (y * ((2 * a) - 1))) by A11, Def1
.= CircleMap . ((1 * (y * ((2 * a) - 1))) + x) by FCONT_1:def 4
.= |[(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:9
.= |[(cos (((2 * PI) * y) * ((2 * a) - 1))),(sin (((2 * PI) * y) * ((2 * a) - 1)))]| by COMPLEX2:8
.= (cLoop y) . ((2 * a) - 1) by A11, Def4
.= ((cLoop x) + (cLoop y)) . a by A10, BORSUK_6:def 2 ; :: thesis: verum

end;

end;

end;

Ciso . x = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop x)) by Def5;
then fX, cLoop x are_homotopic by A1, TOPALG_1:46;
then A12: fX + fY,(cLoop x) + (cLoop y) are_homotopic by A4, BORSUK_6:76;
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:63
.= (Ciso . x) * (Ciso . y) by A3, A12, TOPALG_1:46 ; :: thesis: verum