let T be DecoratedTree; :: thesis: roots <*T*> = <*(T . {})*>
A1: dom <*T*> = Seg 1 by FINSEQ_1:def 8;
A2: dom <*(T . {})*> = Seg 1 by FINSEQ_1:def 8;
A3: <*T*> . 1 = T ;
A4: <*(T . {})*> . 1 = T . {} ;

now :: thesis: for i being Element of NAT st i in dom <*T*> holds
ex t being DecoratedTree st
( t = <*T*> . i & <*(T . {})*> . i = t . {} )

let i be Element of NAT ; :: thesis: ( i in dom <*T*> implies ex t being DecoratedTree st
( t = <*T*> . i & <*(T . {})*> . i = t . {} ) )
assume A5: 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, A3, A4, A5, FINSEQ_1:2, TARSKI:def 1; :: thesis: verum

end;

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