let x, y be object ; :: thesis: ( <*x,y*> is FinTree-yielding iff ( x is finite Tree & y is finite Tree ) )
A1: ( ( x is finite Tree & y is finite Tree ) iff {x,y} is constituted-FinTrees ) by Th16;
rng <*x,y*> = {x,y} by FINSEQ_2:127;
hence ( <*x,y*> is FinTree-yielding iff ( x is finite Tree & y is finite Tree ) ) by A1; :: thesis: verum