theorem Th13: :: FLANG_1:13

for E being set
for A being Subset of (E ^omega) holds
( A ^^ {(<%> E)} = A & {(<%> E)} ^^ A = A )