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 A2: h = pi_1-iso P ; :: thesis: h is bijective
A3: h is one-to-one by A1, A2, Th52;
h is onto by A1, A2, Th53;
then rng h = the carrier of (pi_1 X,x0) by FUNCT_2:def 3;
hence h is bijective by A3, GROUP_6:70; :: thesis: verum