theorem Th23: :: FUNCT_7:23

for p, q being FinSequence st p ^ q is Function-yielding holds
( p is Function-yielding & q is Function-yielding )