let f be Function; :: thesis: sproduct f c= PFuncs (dom f),(union (rng f))
let x be set ; :: 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 Th68;
hence x in PFuncs (dom f),(union (rng f)) by PARTFUN1:119; :: thesis: verum