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