theorem Th117: :: FINSEQ_3:119

for A being set
for i being Nat holds
( ( i <> 0 & A = {} ) iff i -tuples_on A = {} )