thus product {} c= {{}} :: according to XBOOLE_0:def 10 :: thesis: {{}} c= product {}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in product {} or x in {{}} )
assume x in product {} ; :: thesis: x in {{}}
then ex g being Function st
( x = g & dom g = dom {} & ( for y being object st y in dom {} holds
g . y in {} . y ) ) by Def5;
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 product {} )
assume x in {{}} ; :: thesis: x in product {}
then A1: x = {} by TARSKI:def 1;
for y being object st y in dom {} holds
{} . y in {} . y ;
hence x in product {} by A1, Th9; :: thesis: verum