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