let S, T be non empty pathwise_connected TopSpace; :: thesis: for s1, s2 being Point of S
for t1, t2 being Point of T holds pi_1 ([:S,T:],[s1,t1]), product <*(pi_1 (S,s2)),(pi_1 (T,t2))*> are_isomorphic
let s1, s2 be Point of S; :: thesis: for t1, t2 being Point of T holds pi_1 ([:S,T:],[s1,t1]), product <*(pi_1 (S,s2)),(pi_1 (T,t2))*> are_isomorphic
let t1, t2 be Point of T; :: thesis: pi_1 ([:S,T:],[s1,t1]), product <*(pi_1 (S,s2)),(pi_1 (T,t2))*> are_isomorphic
( pi_1 (S,s1), pi_1 (S,s2) are_isomorphic & pi_1 (T,t1), pi_1 (T,t2) are_isomorphic ) by TOPALG_3:33;
then A1: product <*(pi_1 (S,s1)),(pi_1 (T,t1))*>, product <*(pi_1 (S,s2)),(pi_1 (T,t2))*> are_isomorphic by Th6;
pi_1 ([:S,T:],[s1,t1]), product <*(pi_1 (S,s1)),(pi_1 (T,t1))*> are_isomorphic by Th30;
hence pi_1 ([:S,T:],[s1,t1]), product <*(pi_1 (S,s2)),(pi_1 (T,t2))*> are_isomorphic by A1, GROUP_6:67; :: thesis: verum