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