set f = Ciso ;
let x, y be Element of INT.Group; :: according to GROUP_6:def 6 :: thesis: Ciso . (x * y) = () * ()
consider fX, fY being Loop of c[10] such that
A1: Ciso . x = Class ((EqRel ((),c[10])),fX) and
A2: Ciso . y = Class ((EqRel ((),c[10])),fY) and
A3: the multF of (pi_1 ((),c[10])) . ((),()) = Class ((EqRel ((),c[10])),(fX + fY)) by TOPALG_1:def 5;
Ciso . y = Class ((EqRel ((),c[10])),()) by Def5;
then A4: fY, cLoop y are_homotopic by ;
reconsider tx = AffineMap (1,x) as Function of R^1,R^1 by TOPMETR:17;
set p = tx * ();
A5: (tx * ()) . 0 = tx . (() . 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 * ()) . 1 = tx . (() . 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 * () as Path of R^1 x, R^1 (x + y) by ;
A7: for a being Point of I[01] holds (CircleMap * (() + p)) . a = (() + ()) . a
proof
let a be Point of I[01]; :: thesis: (CircleMap * (() + p)) . a = (() + ()) . a
per cases ( a <= 1 / 2 or 1 / 2 <= a ) ;
suppose A8: a <= 1 / 2 ; :: thesis: (CircleMap * (() + p)) . a = (() + ()) . a
then A9: 2 * a is Point of I[01] by BORSUK_6:3;
thus (CircleMap * (() + p)) . a = CircleMap . ((() + p) . a) by FUNCT_2:15
.= CircleMap . (() . (2 * a)) by
.= CircleMap . (x * (2 * a)) by
.= |[(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)))]|
.= () . (2 * a) by
.= (() + ()) . a by ; :: thesis: verum
end;
suppose A10: 1 / 2 <= a ; :: thesis: (CircleMap * (() + p)) . a = (() + ()) . a
then A11: (2 * a) - 1 is Point of I[01] by BORSUK_6:4;
thus (CircleMap * (() + p)) . a = CircleMap . ((() + p) . a) by FUNCT_2:15
.= CircleMap . (p . ((2 * a) - 1)) by
.= CircleMap . (tx . (() . ((2 * a) - 1))) by
.= CircleMap . (tx . (y * ((2 * a) - 1))) by
.= 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
.= () . ((2 * a) - 1) by
.= (() + ()) . a by ; :: thesis: verum
end;
end;
end;
Ciso . x = Class ((EqRel ((),c[10])),()) by Def5;
then fX, cLoop x are_homotopic by ;
then A12: fX + fY,() + () are_homotopic by ;
thus Ciso . (x * y) = Class ((EqRel ((),c[10])),(CircleMap * (() + p))) by Th25
.= Class ((EqRel ((),c[10])),(() + ())) by
.= () * () by ; :: thesis: verum