let X be non empty TopSpace; :: thesis: for x0, x1 being Point of
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 ; :: 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