for X being non empty TopSpace
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 Homomorphism of (pi_1 (X,x1)),(pi_1 (X,x0))