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