let S, T be 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
let s be 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 t be Point of T; pi_1 ([:S,T:],[s,t]), product <*(pi_1 (S,s)),(pi_1 (T,t))*> are_isomorphic
take
FGPrIso (s,t)
; GROUP_6:def 11 FGPrIso (s,t) is bijective
thus
FGPrIso (s,t) is bijective
; verum