let X be non empty TopSpace; 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; 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; 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 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));
( 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
;
g * h = hA3:
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
;
verum end;
hence
1_ (pi_1 (X,a)) = Class ((EqRel (X,a)),C)
by GROUP_1:4; verum