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;
consider s being Element of {} * such that
A4: ( s = x & len s = n ) by A3;
thus contradiction by A1, A4; :: thesis: verum