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