let X be non empty TopSpace; :: thesis: 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; :: thesis: 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; :: thesis: ( x0,x1 are_connected implies pi_1-iso P is one-to-one )
assume A1: x0,x1 are_connected ; :: thesis: pi_1-iso P is one-to-one
set f = pi_1-iso P;
let a, b be set ; :: according to FUNCT_1:def 8 :: thesis: ( not a in K1((pi_1-iso P)) or not b in K1((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 ; :: thesis: a = b
consider A being Loop of x1 such that
A5: a = Class (EqRel X,x1),A by A2, Th48;
consider B being Loop of x1 such that
A6: b = Class (EqRel X,x1),B by A3, Th48;
A7: (pi_1-iso P) . a = Class (EqRel X,x0),((P + A) + (- P)) by A1, A5, Def4;
(pi_1-iso P) . b = Class (EqRel X,x0),((P + B) + (- P)) by A1, A6, Def4;
then (P + A) + (- P),(P + B) + (- P) are_homotopic by A4, A7, Th47;
then P + A,P + B are_homotopic by A1, Th28;
then A,B are_homotopic by A1, Th30;
hence a = b by A5, A6, Th47; :: thesis: verum