let X be non empty TopSpace; :: thesis: for x0, x1 being Point of X
for P, Q being Path of x0,x1 st x0,x1 are_connected & P,Q are_homotopic holds
pi_1-iso P = pi_1-iso Q
let x0, x1 be Point of X; :: thesis: for P, Q being Path of x0,x1 st x0,x1 are_connected & P,Q are_homotopic holds
pi_1-iso P = pi_1-iso Q
let P, Q be Path of x0,x1; :: thesis: ( x0,x1 are_connected & P,Q are_homotopic implies pi_1-iso P = pi_1-iso Q )
assume that
A1: x0,x1 are_connected and
A2: P,Q are_homotopic ; :: thesis: pi_1-iso P = pi_1-iso Q
for x being Element of (pi_1 X,x1) holds (pi_1-iso P) . x = (pi_1-iso Q) . x

proof

A3: - P, - Q are_homotopic by A1, A2, BORSUK_6:85;
let x be Element of (pi_1 X,x1); :: thesis: (pi_1-iso P) . x = (pi_1-iso Q) . x
consider L being Loop of x1 such that
A4: x = Class (EqRel X,x1),L by Th48;
L,L are_homotopic by BORSUK_2:15;
then P + L,Q + L are_homotopic by A1, A2, BORSUK_6:83;
then A5: (P + L) + (- P),(Q + L) + (- Q) are_homotopic by A1, A3, BORSUK_6:83;
thus (pi_1-iso P) . x = Class (EqRel X,x0),((P + L) + (- P)) by A1, A4, Def6
.= Class (EqRel X,x0),((Q + L) + (- Q)) by A5, Th47
.= (pi_1-iso Q) . x by A1, A4, Def6 ; :: thesis: verum

end;

hence pi_1-iso P = pi_1-iso Q by FUNCT_2:113; :: thesis: verum