let T be DecoratedTree; :: thesis: roots <*T*> = <*(T . {} )*>
A1: ( dom <*T*> = Seg 1 & dom <*(T . {} )*> = Seg 1 & <*T*> is DTree-yielding & <*T*> . 1 = T & <*(T . {} )*> . 1 = T . {} ) by FINSEQ_1:def 8;

now

let i be Element of NAT ; :: thesis: ( i in dom <*T*> implies ex t being DecoratedTree st
( t = <*T*> . i & <*(T . {} )*> . i = t . {} ) )
assume A2: i in dom <*T*> ; :: thesis: ex t being DecoratedTree st
( t = <*T*> . i & <*(T . {} )*> . i = t . {} )
take t = T; :: thesis: ( t = <*T*> . i & <*(T . {} )*> . i = t . {} )
thus ( t = <*T*> . i & <*(T . {} )*> . i = t . {} ) by A1, A2, FINSEQ_1:4, TARSKI:def 1; :: thesis: verum

end;

hence roots <*T*> = <*(T . {} )*> by A1, TREES_3:def 18; :: thesis: verum