theorem Th30: :: TOPALG_4:30

for S, T being non empty TopSpace
for s being Point of S
for t being Point of T holds pi_1 ([:S,T:],[s,t]), product <*(pi_1 (S,s)),(pi_1 (T,t))*> are_isomorphic