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 that
A1: x = Class (EqRel X,a),P and
A2: y = Class (EqRel X,a),(- P) ; :: thesis: x " = y
consider C being constant Loop of a;
A3: P + (- P),C are_homotopic by BORSUK_6:92;
A4: (- P) + P,C are_homotopic by BORSUK_6:94;

now

thus x * y = Class (EqRel X,a),(P + (- P)) by A1, A2, Lm3
.= Class (EqRel X,a),C by A3, Th47
.= 1_ (pi_1 X,a) by Th63 ; :: thesis: y * x = 1_ (pi_1 X,a)
thus y * x = Class (EqRel X,a),((- P) + P) by A1, A2, Lm3
.= Class (EqRel X,a),C by A4, Th47
.= 1_ (pi_1 X,a) by Th63 ; :: thesis: verum

end;

hence x " = y by GROUP_1:def 6; :: thesis: verum