for S, T being non empty TopSpace
for s1, s2 being Point of S
for t1, t2 being Point of T
for f being Homomorphism of (pi_1 (S,s1)),(pi_1 (S,s2))
for g being Homomorphism of (pi_1 (T,t1)),(pi_1 (T,t2)) st f is bijective & g is bijective holds
(Gr2Iso (f,g)) * (FGPrIso (s1,t1)) is bijective