consider C being constant Loop of a;
set E = EqRel (X,a);
set G = pi_1 (X,a);
set e = Class ((EqRel (X,a)),C);
C in Loops a by Def1;
then A1: Class ((EqRel (X,a)),C) in Class (EqRel (X,a)) by EQREL_1:def 5;
thus pi_1 (X,a) is associative :: thesis: pi_1 (X,a) is Group-like

proof

let x, y, z be Element of (pi_1 (X,a)); :: according to GROUP_1:def 4 :: thesis: (x * y) * z = x * (y * z)
consider A being Loop of a such that
A2: x = Class ((EqRel (X,a)),A) by Th48;
consider B being Loop of a such that
A3: y = Class ((EqRel (X,a)),B) by Th48;
consider BC being Loop of a such that
A4: y * z = Class ((EqRel (X,a)),BC) by Th48;
consider C being Loop of a such that
A5: z = Class ((EqRel (X,a)),C) by Th48;
y * z = Class ((EqRel (X,a)),(B + C)) by A3, A5, Lm4;
then ( A,A are_homotopic & BC,B + C are_homotopic ) by A4, Th47, BORSUK_2:15;
then A6: A + BC,A + (B + C) are_homotopic by BORSUK_6:83;
consider AB being Loop of a such that
A7: x * y = Class ((EqRel (X,a)),AB) by Th48;
x * y = Class ((EqRel (X,a)),(A + B)) by A2, A3, Lm4;
then ( C,C are_homotopic & AB,A + B are_homotopic ) by A7, Th47, BORSUK_2:15;
then A8: AB + C,(A + B) + C are_homotopic by BORSUK_6:83;
A9: (A + B) + C,A + (B + C) are_homotopic by BORSUK_6:81;
thus (x * y) * z = Class ((EqRel (X,a)),(AB + C)) by A5, A7, Lm4
.= Class ((EqRel (X,a)),((A + B) + C)) by A8, Th47
.= Class ((EqRel (X,a)),(A + (B + C))) by A9, Th47
.= Class ((EqRel (X,a)),(A + BC)) by A6, Th47
.= x * (y * z) by A2, A4, Lm4 ; :: thesis: verum

end;

reconsider e = Class ((EqRel (X,a)),C) as Element of (pi_1 (X,a)) by A1, Def5;
take e ; :: according to GROUP_1:def 3 :: thesis: for b₁ being Element of the carrier of (pi_1 (X,a)) holds
( b₁ * e = b₁ & e * b₁ = b₁ & ex b₂ being Element of the carrier of (pi_1 (X,a)) st
( b₁ * b₂ = e & b₂ * b₁ = e ) )
let h be Element of (pi_1 (X,a)); :: thesis: ( h * e = h & e * h = h & ex b₁ being Element of the carrier of (pi_1 (X,a)) st
( h * b₁ = e & b₁ * h = e ) )
consider A being Loop of a such that
A10: h = Class ((EqRel (X,a)),A) by Th48;
A11: A + C,A are_homotopic by BORSUK_6:88;
thus h * e = Class ((EqRel (X,a)),(A + C)) by A10, Lm4
.= h by A10, A11, Th47 ; :: thesis: ( e * h = h & ex b₁ being Element of the carrier of (pi_1 (X,a)) st
( h * b₁ = e & b₁ * h = e ) )
A12: C + A,A are_homotopic by BORSUK_6:90;
thus e * h = Class ((EqRel (X,a)),(C + A)) by A10, Lm4
.= h by A10, A12, Th47 ; :: thesis: ex b₁ being Element of the carrier of (pi_1 (X,a)) st
( h * b₁ = e & b₁ * h = e )
set x = Class ((EqRel (X,a)),(- A));
- A in Loops a by Def1;
then Class ((EqRel (X,a)),(- A)) in Class (EqRel (X,a)) by EQREL_1:def 5;
then reconsider x = Class ((EqRel (X,a)),(- A)) as Element of (pi_1 (X,a)) by Def5;
take x ; :: thesis: ( h * x = e & x * h = e )
A13: A + (- A),C are_homotopic by BORSUK_6:92;
thus h * x = Class ((EqRel (X,a)),(A + (- A))) by A10, Lm4
.= e by A13, Th47 ; :: thesis: x * h = e
A14: (- A) + A,C are_homotopic by BORSUK_6:94;
thus x * h = Class ((EqRel (X,a)),((- A) + A)) by A10, Lm4
.= e by A14, Th47 ; :: thesis: verum