theorem Th5: :: FLANG_1:5

for E being set
for a being Element of E ^omega
for p, q being XFinSequence st a = p ^ q holds
( p is Element of E ^omega & q is Element of E ^omega )