let X be set ; :: thesis: Funcs {} ,X = {{} }
thus Funcs {} ,X c= {{} } :: according to XBOOLE_0:def 10 :: thesis: {{} } c= Funcs {} ,X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Funcs {} ,X or x in {{} } )
assume x in Funcs {} ,X ; :: thesis: x in {{} }
then ex f being Function st
( x = f & dom f = {} & rng f c= X ) by FUNCT_2:def 2;
then x = {} ;
hence x in {{} } by TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {{} } or x in Funcs {} ,X )
assume x in {{} } ; :: thesis: x in Funcs {} ,X
then ( x = {} & dom {} = {} & rng {} = {} & {} c= X ) by TARSKI:def 1, XBOOLE_1:2;
hence x in Funcs {} ,X by FUNCT_2:def 2; :: thesis: verum