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;
consider p being Element of B;
( B = { s where s is Element of A * : len s = i } & p in B ) ;
then ex s being Element of A * st
( p = s & len s = i ) ;
then 1 in dom p by A1, Th27;
then X: rng p <> {} by RELAT_1:65;
thus contradiction by A2, X; :: thesis: verum

end;

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