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 Th48;
set E = EqRel X,a;

now

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 Th48;
A2: P,P + C are_homotopic by BORSUK_6:88;
thus h * g = Class (EqRel X,a),(P + C) by A1, Lm4
.= h by A1, A2, Th47 ; :: thesis: g * h = h
A3: P,C + P are_homotopic by BORSUK_6:90;
thus g * h = Class (EqRel X,a),(C + P) by A1, Lm4
.= h by A1, A3, Th47 ; :: thesis: verum

end;

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