theorem Th43: :: FLEXARY1:43
for f, g being FinSequence st f ^ g is FinSequence-yielding holds
( f is FinSequence-yielding & g is FinSequence-yielding )