let S, T be non empty TopSpace; :: thesis: for s being Point of
for t being Point of holds FGPrIso s,t is bijective
let s be Point of ; :: thesis: for t being Point of holds FGPrIso s,t is bijective
let t be Point of ; :: 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