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