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
for h being Homomorphism of (pi_1 (X,x1)),(pi_1 (X,x0)) st h = pi_1-iso P holds
h is bijective
let x0, x1 be Point of X; :: thesis: for P being Path of x0,x1 st x0,x1 are_connected holds
for h being Homomorphism of (pi_1 (X,x1)),(pi_1 (X,x0)) st h = pi_1-iso P holds
h is bijective
let P be Path of x0,x1; :: thesis: ( x0,x1 are_connected implies for h being Homomorphism of (pi_1 (X,x1)),(pi_1 (X,x0)) st h = pi_1-iso P holds
h is bijective )
assume A1: x0,x1 are_connected ; :: thesis: for h being Homomorphism of (pi_1 (X,x1)),(pi_1 (X,x0)) st h = pi_1-iso P holds
h is bijective
let h be Homomorphism of (pi_1 (X,x1)),(pi_1 (X,x0)); :: thesis: ( h = pi_1-iso P implies h is bijective )
assume h = pi_1-iso P ; :: thesis: h is bijective
then ( h is one-to-one & h is onto ) by A1, Th52, Th53;
hence h is bijective ; :: thesis: verum