let S, T be non empty TopSpace; :: thesis: 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
let s be Point of S; :: thesis: for t being Point of T holds pi_1 [:S,T:],[s,t], product <*(pi_1 S,s),(pi_1 T,t)*> are_isomorphic
let t be Point of T; :: thesis: pi_1 [:S,T:],[s,t], product <*(pi_1 S,s),(pi_1 T,t)*> are_isomorphic
take FGPrIso s,t ; :: according to GROUP_6:def 15 :: thesis: FGPrIso s,t is bijective
thus FGPrIso s,t is bijective by Th29; :: thesis: verum