let X be set ; :: thesis: 0 -tuples_on X = {{} }
set S = { s where s is Element of X * : len s = 0 } ;

now

let x be set ; :: thesis: ( ( x in { s where s is Element of X * : len s = 0 } implies x in {{} } ) & ( x in {{} } implies x in { s where s is Element of X * : len s = 0 } ) )

hereby :: thesis: ( x in {{} } implies x in { s where s is Element of X * : len s = 0 } )

assume x in { s where s is Element of X * : len s = 0 } ; :: thesis: x in {{} }
then consider s being Element of X * such that
A2: ( x = s & len s = 0 ) ;
s = {} by A2;
hence x in {{} } by A2, TARSKI:def 1; :: thesis: verum

end;

assume x in {{} } ; :: thesis: x in { s where s is Element of X * : len s = 0 }
then A3: x = {} by TARSKI:def 1;
<*> (X * ) is Element of X * by FINSEQ_1:66;
hence x in { s where s is Element of X * : len s = 0 } by A3, CARD_1:47; :: thesis: verum

end;

hence 0 -tuples_on X = {{} } by TARSKI:2; :: thesis: verum