theorem Th41: :: FLANG_1:41

for E, x being set
for A being Subset of (E ^omega) holds
( x in A * iff ex n being Nat st x in A |^ n )