let n be Element of NAT ; :: thesis: ( n <> 0 implies n -tuples_on {} = {} )
assume that
A1: n <> 0 and
A2: n -tuples_on {} <> {} ; :: thesis: contradiction
consider x being set such that
A3: x in n -tuples_on {} by A2, XBOOLE_0:def 1;
ex s being Element of {} * st
( s = x & len s = n ) by A3;
hence contradiction by A1; :: thesis: verum