for S, T being non empty TopSpace
for s being Point of S
for t being Point of T
for f being continuous Function of S,T
for P being Path of t,f . s
for h being Homomorphism of (pi_1 (S,s)),(pi_1 (T,t)) st f is being_homeomorphism & f . s,t are_connected & h = (pi_1-iso P) * (FundGrIso (f,s)) holds
h is bijective