sproduct {} c= PFuncs ({},{}) by Th55, RELAT_1:38, ZFMISC_1:2;
hence sproduct {} c= {{}} by PARTFUN1:48; :: according to XBOOLE_0:def 10 :: thesis: {{}} c= sproduct {}
let x be object ; :: 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 Th50; :: thesis: verum