let x be set ; :: thesis: for i being Element of NAT st i <> 0 holds
( i |-> x is Tree-yielding iff x is Tree )
let i be Element of NAT ; :: thesis: ( i <> 0 implies ( i |-> x is Tree-yielding iff x is Tree ) )
assume i <> 0 ; :: thesis: ( i |-> x is Tree-yielding iff x is Tree )
then ( i |-> x = (Seg i) --> x & Seg i <> {} ) by FINSEQ_2:def 2;
then rng (i |-> x) = {x} by FUNCOP_1:14;
then ( ( x is Tree implies rng (i |-> x) is constituted-Trees ) & ( rng (i |-> x) is constituted-Trees implies x is Tree ) & ( i |-> x is Tree-yielding implies rng (i |-> x) is constituted-Trees ) & ( rng (i |-> x) is constituted-Trees implies i |-> x is Tree-yielding ) ) by Def9, Th13;
hence ( i |-> x is Tree-yielding iff x is Tree ) ; :: thesis: verum