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 E = EqRel X,a;
set G = pi_1 X,a;
reconsider g = Class (EqRel X,a),C as Element of (pi_1 X,a) by Th48;
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, Lm3
.=
h
by A1, A2, Th47
;
:: thesis: g * h = hA3:
P,
C + P are_homotopic
by BORSUK_6:90;
thus g * h =
Class (EqRel X,a),
(C + P)
by A1, Lm3
.=
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