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