let S, T be non empty TopSpace; :: thesis: 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; :: thesis: 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; :: thesis: 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)); :: thesis: 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)); :: thesis: ( f is bijective & g is bijective implies (Gr2Iso (f,g)) * (FGPrIso (s1,t1)) is bijective )
assume ( f is bijective & g is bijective ) ; :: thesis: (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; :: thesis: verum