theorem Th25: :: TREES_3:25

for p, q being FinSequence holds
( ( p is Tree-yielding & q is Tree-yielding ) iff p ^ q is Tree-yielding )