let S, T be non empty pathwise_connected TopSpace; 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; 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; 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; verum