let S, T be non empty TopSpace; :: thesis: for s being Point of S
for t being Point of T holds FGPrIso s,t is bijective
let s be Point of S; :: thesis: for t being Point of T holds FGPrIso s,t is bijective
let t be Point of T; :: thesis: FGPrIso s,t is bijective
thus FGPrIso s,t is one-to-one ; :: according to FUNCT_2:def 4 :: thesis: FGPrIso s,t is onto
thus rng (FGPrIso s,t) = the carrier of (product <*(pi_1 S,s),(pi_1 T,t)*>) by FUNCT_2:def 3; :: according to FUNCT_2:def 3 :: thesis: verum