theorem Th31: :: FLANG_2:31

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