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