theorem Th15: :: FLANG_3:15

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