theorem Th40: :: FLANG_1:40

for E being set
for C being Subset of (E ^omega)
for a, b being Element of E ^omega
for n, m being Nat st a in C |^ m & b in C |^ n holds
a ^ b in C |^ (m + n)