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 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