let S, T be 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
let s1, s2 be 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
let t1, t2 be 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
let f be 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
let g be Homomorphism of (pi_1 (T,t1)),(pi_1 (T,t2)); ( f is bijective & g is bijective implies (Gr2Iso (f,g)) * (FGPrIso (s1,t1)) is bijective )
assume
( f is bijective & g is bijective )
; (Gr2Iso (f,g)) * (FGPrIso (s1,t1)) is bijective
then A1:
Gr2Iso (f,g) is bijective
by Th5;
FGPrIso (s1,t1) is bijective
;
hence
(Gr2Iso (f,g)) * (FGPrIso (s1,t1)) is bijective
by A1, GROUP_6:64; verum