let x be set ; :: thesis: for i being Element of NAT st i <> 0 holds
( i |-> x is DTree-yielding iff x is DecoratedTree )
let i be Element of NAT ; :: thesis: ( i <> 0 implies ( i |-> x is DTree-yielding iff x is DecoratedTree ) )
assume i <> 0 ; :: thesis: ( i |-> x is DTree-yielding iff x is DecoratedTree )
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 DecoratedTree implies rng (i |-> x) is constituted-DTrees ) & ( rng (i |-> x) is constituted-DTrees implies x is DecoratedTree ) & ( i |-> x is DTree-yielding implies rng (i |-> x) is constituted-DTrees ) & ( rng (i |-> x) is constituted-DTrees implies i |-> x is DTree-yielding ) ) by Def11, Th15;
hence ( i |-> x is DTree-yielding iff x is DecoratedTree ) ; :: thesis: verum