let p, q be FinSequence; :: thesis: ( ( p is Tree-yielding & q is Tree-yielding ) iff p ^ q is Tree-yielding )
A1: rng (p ^ q) = (rng p) \/ (rng q) by FINSEQ_1:31;
thus ( p is Tree-yielding & q is Tree-yielding implies p ^ q is Tree-yielding ) by A1, Th3; :: thesis: ( p ^ q is Tree-yielding implies ( p is Tree-yielding & q is Tree-yielding ) )
assume A2: rng (p ^ q) is constituted-Trees ; :: according to TREES_3:def 9 :: thesis: ( p is Tree-yielding & q is Tree-yielding )
hence rng p is constituted-Trees by A1, Th3; :: according to TREES_3:def 9 :: thesis: q is Tree-yielding
thus rng q is constituted-Trees by A1, A2, Th3; :: according to TREES_3:def 9 :: thesis: verum