let S, T be non empty TopSpace; :: thesis: for s1, s2 being Point of
for t1, t2 being Point of
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 ; :: thesis: for t1, t2 being Point of
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 ; :: 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 by Th29;
hence (Gr2Iso f,g) * (FGPrIso s1,t1) is bijective by A1, GROUP_6:74; :: thesis: verum