sproduct {} c= PFuncs {} ,{} by Th71, RELAT_1:60, ZFMISC_1:2;
hence sproduct {} c= {{} } by PARTFUN1:122; :: according to XBOOLE_0:def 10 :: thesis: {{} } c= sproduct {}
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {{} } or x in sproduct {} )
assume x in {{} } ; :: thesis: x in sproduct {}
then x = {} by TARSKI:def 1;
hence x in sproduct {} by Th66; :: thesis: verum