let x, y be set ; :: thesis: ( <*x,y*> is FinTree-yielding iff ( x is finite Tree & y is finite Tree ) )
( ( x is finite Tree & y is finite Tree implies {x,y} is constituted-FinTrees ) & ( {x,y} is constituted-FinTrees implies ( x is finite Tree & y is finite Tree ) ) & rng <*x,y*> = {x,y} ) by Th17, FINSEQ_2:147;
hence ( <*x,y*> is FinTree-yielding iff ( x is finite Tree & y is finite Tree ) ) by Def10; :: thesis: verum