theorem Th37: :: FLANG_3:37

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