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 11 :: thesis: FGPrIso (s,t) is bijective
thus FGPrIso (s,t) is bijective ; :: thesis: verum