let X be non empty TopSpace; for a being Point of X
for x, y being Element of (pi_1 (X,a))
for P being Loop of a st x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),(- P)) holds
x " = y
let a be Point of X; for x, y being Element of (pi_1 (X,a))
for P being Loop of a st x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),(- P)) holds
x " = y
set E = EqRel (X,a);
set G = pi_1 (X,a);
let x, y be Element of (pi_1 (X,a)); for P being Loop of a st x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),(- P)) holds
x " = y
let P be Loop of a; ( x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),(- P)) implies x " = y )
assume A1:
( x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),(- P)) )
; x " = y
set C = the constant Loop of a;
A2:
(- P) + P, the constant Loop of a are_homotopic
by BORSUK_6:86;
A3: y * x =
Class ((EqRel (X,a)),((- P) + P))
by A1, Lm4
.=
Class ((EqRel (X,a)), the constant Loop of a)
by A2, Th46
.=
1_ (pi_1 (X,a))
by Th62
;
A4:
P + (- P), the constant Loop of a are_homotopic
by BORSUK_6:84;
x * y =
Class ((EqRel (X,a)),(P + (- P)))
by A1, Lm4
.=
Class ((EqRel (X,a)), the constant Loop of a)
by A4, Th46
.=
1_ (pi_1 (X,a))
by Th62
;
hence
x " = y
by A3, GROUP_1:def 5; verum