let X be set ; :: thesis: 0 -tuples_on X = {{}}
set S = { s where s is Element of X * : len s = 0 } ;
now :: thesis: for x being object holds
( ( 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 } ) )
let x be object ; :: 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
A1: x = s and
A2: len s = 0 ;
s = {} by A2;
hence x in {{}} by A1, 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:49;
hence x in { s where s is Element of X * : len s = 0 } by A3, CARD_1:27; :: thesis: verum
end;
hence 0 -tuples_on X = {{}} by TARSKI:2; :: thesis: verum