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 by Th29;
hence (Gr2Iso f,g) * (FGPrIso s1,t1) is bijective by A1, GROUP_6:74; :: thesis: verum