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 ) :: thesis: ( p ^ q is DTree-yielding implies ( p is DTree-yielding & q is DTree-yielding ) )

proof

assume that
A2: rng p is constituted-DTrees and
A3: rng q is constituted-DTrees ; :: according to TREES_3:def 11 :: thesis: p ^ q is DTree-yielding
thus rng (p ^ q) is constituted-DTrees by A1, A2, A3, Th9; :: according to TREES_3:def 11 :: thesis: verum

end;

assume A4: 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, A4, Th9; :: according to TREES_3:def 11 :: thesis: verum