let X be non empty TopSpace; for x0, x1 being Point of X
for P being Path of x0,x1 st x0,x1 are_connected holds
pi_1-iso P is one-to-one
let x0, x1 be Point of X; for P being Path of x0,x1 st x0,x1 are_connected holds
pi_1-iso P is one-to-one
let P be Path of x0,x1; ( x0,x1 are_connected implies pi_1-iso P is one-to-one )
assume A1:
x0,x1 are_connected
; pi_1-iso P is one-to-one
set f = pi_1-iso P;
let a, b be object ; FUNCT_1:def 4 ( not a in K49((pi_1-iso P)) or not b in K49((pi_1-iso P)) or not (pi_1-iso P) . a = (pi_1-iso P) . b or a = b )
assume that
A2:
a in dom (pi_1-iso P)
and
A3:
b in dom (pi_1-iso P)
and
A4:
(pi_1-iso P) . a = (pi_1-iso P) . b
; a = b
consider B being Loop of x1 such that
A5:
b = Class ((EqRel (X,x1)),B)
by A3, Th47;
A6:
(pi_1-iso P) . b = Class ((EqRel (X,x0)),((P + B) + (- P)))
by A1, A5, Def6;
consider A being Loop of x1 such that
A7:
a = Class ((EqRel (X,x1)),A)
by A2, Th47;
(pi_1-iso P) . a = Class ((EqRel (X,x0)),((P + A) + (- P)))
by A1, A7, Def6;
then
(P + A) + (- P),(P + B) + (- P) are_homotopic
by A4, A6, Th46;
then
P + A,P + B are_homotopic
by A1, Th27;
then
A,B are_homotopic
by A1, Th29;
hence
a = b
by A7, A5, Th46; verum