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
consider C being constant Loop of a;
A2: (- P) + P,C are_homotopic by BORSUK_6:94;
A3: y * x = Class ((EqRel (X,a)),((- P) + P)) by A1, Lm4
.= Class ((EqRel (X,a)),C) by A2, Th47
.= 1_ (pi_1 (X,a)) by Th63 ;
A4: P + (- P),C are_homotopic by BORSUK_6:92;
x * y = Class ((EqRel (X,a)),(P + (- P))) by A1, Lm4
.= Class ((EqRel (X,a)),C) by A4, Th47
.= 1_ (pi_1 (X,a)) by Th63 ;
hence x " = y by A3, GROUP_1:def 6; :: thesis: verum