theorem Th21: :: FLANG_2:21

for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds
( A |^ (m,n) = {} iff ( m > n or ( m > 0 & A = {} ) ) )