for S, T being 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