let f be Function; :: thesis: sproduct f c= PFuncs ((dom f),(union (rng f)))
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in sproduct f or x in PFuncs ((dom f),(union (rng f))) )
assume x in sproduct f ; :: thesis: x in PFuncs ((dom f),(union (rng f)))
then x is PartFunc of (dom f),(union (rng f)) by Th52;
hence x in PFuncs ((dom f),(union (rng f))) by PARTFUN1:45; :: thesis: verum