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 object ; :: according to FUNCT_1:def 4 :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum