let S, T be non empty arcwise_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:35;
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:78; :: thesis: verum