let X be non empty TopSpace; :: thesis: 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; :: thesis: 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)); :: thesis: 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; :: thesis: ( 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)) ) ; :: thesis: 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; :: thesis: verum