let x be object ; :: thesis: for i being Nat st i <> 0 holds
( i |-> x is FinTree-yielding iff x is finite Tree )
let i be Nat; :: thesis: ( i <> 0 implies ( i |-> x is FinTree-yielding iff x is finite Tree ) )
assume A1: i <> 0 ; :: thesis: ( i |-> x is FinTree-yielding iff x is finite Tree )
i |-> x = (Seg i) --> x by FINSEQ_2:def 2;
then rng (i |-> x) = {x} by A1, FUNCOP_1:8;
then ( x is finite Tree iff rng (i |-> x) is constituted-FinTrees ) by Th13;
hence ( i |-> x is FinTree-yielding iff x is finite Tree ) ; :: thesis: verum