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 object ; :: 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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in {{}} or x in Funcs ({},X) )
A1: {} c= X ;
assume x in {{}} ; :: thesis: x in Funcs ({},X)
then A2: x = {} by TARSKI:def 1;
( dom {} = {} & rng {} = {} ) ;
hence x in Funcs ({},X) by A2, A1, FUNCT_2:def 2; :: thesis: verum