let X be non empty TopSpace; :: thesis: for a being Point of X
for C being constant Loop of a holds 1_ (pi_1 (X,a)) = Class ((EqRel (X,a)),C)
let a be Point of X; :: thesis: for C being constant Loop of a holds 1_ (pi_1 (X,a)) = Class ((EqRel (X,a)),C)
let C be constant Loop of a; :: thesis: 1_ (pi_1 (X,a)) = Class ((EqRel (X,a)),C)
set G = pi_1 (X,a);
reconsider g = Class ((EqRel (X,a)),C) as Element of (pi_1 (X,a)) by Th47;
set E = EqRel (X,a);

now :: thesis: for h being Element of (pi_1 (X,a)) holds
( h * g = h & g * h = h )

let h be Element of (pi_1 (X,a)); :: thesis: ( h * g = h & g * h = h )
consider P being Loop of a such that
A1: h = Class ((EqRel (X,a)),P) by Th47;
A2: P,P + C are_homotopic by BORSUK_6:80;
thus h * g = Class ((EqRel (X,a)),(P + C)) by A1, Lm4
.= h by A1, A2, Th46 ; :: thesis: g * h = h
A3: P,C + P are_homotopic by BORSUK_6:82;
thus g * h = Class ((EqRel (X,a)),(C + P)) by A1, Lm4
.= h by A1, A3, Th46 ; :: thesis: verum

end;

hence 1_ (pi_1 (X,a)) = Class ((EqRel (X,a)),C) by GROUP_1:4; :: thesis: verum