let A be set ; :: thesis: for i being Nat holds
( ( i <> 0 & A = {} ) iff i -tuples_on A = {} )
let i be Nat; :: thesis: ( ( i <> 0 & A = {} ) iff i -tuples_on A = {} )

hereby :: thesis: ( i -tuples_on A = {} implies ( i <> 0 & A = {} ) )

assume i <> 0 ; :: thesis: ( A = {} implies not i -tuples_on A <> {} )
then A1: 0 + 1 <= i by NAT_1:13;
assume that
A2: A = {} and
A3: i -tuples_on A <> {} ; :: thesis: contradiction
reconsider B = i -tuples_on A as non empty FinSequenceSet of A by A3;
set p = the Element of B;
( B = { s where s is Element of A * : len s = i } & the Element of B in B ) ;
then ex s being Element of A * st
( the Element of B = s & len s = i ) ;
then 1 in dom the Element of B by A1, Th25;
then A4: rng the Element of B <> {} by RELAT_1:42;
thus contradiction by A2, A4; :: thesis: verum

end;

assume that
A5: i -tuples_on A = {} and
A6: ( i = 0 or A <> {} ) ; :: thesis: contradiction
len (<*> A) = 0 ;
then reconsider A = A as non empty set by A5, A6, FINSEQ_2:133;
not i -tuples_on A is empty ;
hence contradiction by A5; :: thesis: verum