theorem :: FLANG_1:29

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