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:77;
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 Th47;
L,L are_homotopic by BORSUK_2:12;
then P + L,Q + L are_homotopic by A1, A2, BORSUK_6:75;
then A5: (P + L) + (- P),(Q + L) + (- Q) are_homotopic by A1, A3, BORSUK_6:75;
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, Th46
.= (pi_1-iso Q) . x by A1, A4, Def6 ; :: thesis: verum

end;

hence pi_1-iso P = pi_1-iso Q ; :: thesis: verum