set C = the constant Loop of a;
set E = EqRel (X,a);
set G = pi_1 (X,a);
set e = Class ((EqRel (X,a)), the constant Loop of a);
the constant Loop of a in Loops a by Def1;
then A1: Class ((EqRel (X,a)), the constant Loop of a) in Class (EqRel (X,a)) by EQREL_1:def 3;
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 3 :: thesis: (x * y) * z = x * (y * z)
consider A being Loop of a such that
A2: x = Class ((EqRel (X,a)),A) by Th47;
consider B being Loop of a such that
A3: y = Class ((EqRel (X,a)),B) by Th47;
consider BC being Loop of a such that
A4: y * z = Class ((EqRel (X,a)),BC) by Th47;
consider C being Loop of a such that
A5: z = Class ((EqRel (X,a)),C) by Th47;
y * z = Class ((EqRel (X,a)),(B + C)) by A3, A5, Lm4;
then ( A,A are_homotopic & BC,B + C are_homotopic ) by A4, Th46, BORSUK_2:12;
then A6: A + BC,A + (B + C) are_homotopic by BORSUK_6:75;
consider AB being Loop of a such that
A7: x * y = Class ((EqRel (X,a)),AB) by Th47;
x * y = Class ((EqRel (X,a)),(A + B)) by A2, A3, Lm4;
then ( C,C are_homotopic & AB,A + B are_homotopic ) by A7, Th46, BORSUK_2:12;
then A8: AB + C,(A + B) + C are_homotopic by BORSUK_6:75;
A9: (A + B) + C,A + (B + C) are_homotopic by BORSUK_6:73;
thus (x * y) * z = Class ((EqRel (X,a)),(AB + C)) by A5, A7, Lm4
.= Class ((EqRel (X,a)),((A + B) + C)) by A8, Th46
.= Class ((EqRel (X,a)),(A + (B + C))) by A9, Th46
.= Class ((EqRel (X,a)),(A + BC)) by A6, Th46
.= x * (y * z) by A2, A4, Lm4 ; :: thesis: verum

end;

reconsider e = Class ((EqRel (X,a)), the constant Loop of a) as Element of (pi_1 (X,a)) by A1, Def5;
take e ; :: according to GROUP_1:def 2 :: 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 Th47;
A11: A + the constant Loop of a,A are_homotopic by BORSUK_6:80;
thus h * e = Class ((EqRel (X,a)),(A + the constant Loop of a)) by A10, Lm4
.= h by A10, A11, Th46 ; :: thesis: ( e * h = h & ex b₁ being Element of the carrier of (pi_1 (X,a)) st
( h * b₁ = e & b₁ * h = e ) )
A12: the constant Loop of a + A,A are_homotopic by BORSUK_6:82;
thus e * h = Class ((EqRel (X,a)),( the constant Loop of a + A)) by A10, Lm4
.= h by A10, A12, Th46 ; :: 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 3;
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), the constant Loop of a are_homotopic by BORSUK_6:84;
thus h * x = Class ((EqRel (X,a)),(A + (- A))) by A10, Lm4
.= e by A13, Th46 ; :: thesis: x * h = e
A14: (- A) + A, the constant Loop of a are_homotopic by BORSUK_6:86;
thus x * h = Class ((EqRel (X,a)),((- A) + A)) by A10, Lm4
.= e by A14, Th46 ; :: thesis: verum