let X be non empty TopSpace; 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; 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; ( 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
; 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));
(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
;
verum
end;
hence
pi_1-iso P = pi_1-iso Q
; verum