let T1, T2 be DecoratedTree; :: thesis: roots <*T1,T2*> = <*(T1 . {}),(T2 . {})*>
A1: len <*T1,T2*> = 2 by FINSEQ_1:44;
A2: len <*(T1 . {}),(T2 . {})*> = 2 by FINSEQ_1:44;
A7: dom <*T1,T2*> = Seg 2 by A1, FINSEQ_1:def 3;
A8: dom <*(T1 . {}),(T2 . {})*> = Seg 2 by A2, FINSEQ_1:def 3;

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

let i be Element of NAT ; :: thesis: ( i in dom <*T1,T2*> implies ex t being DecoratedTree st
( t = <*T1,T2*> . i & <*(T1 . {}),(T2 . {})*> . i = t . {} ) )
assume i in dom <*T1,T2*> ; :: thesis: ex t being DecoratedTree st
( t = <*T1,T2*> . i & <*(T1 . {}),(T2 . {})*> . i = t . {} )
then i in Seg 2 by A1, FINSEQ_1:def 3;
then ( i = 1 or i = 2 ) by FINSEQ_1:2, TARSKI:def 2;
hence ex t being DecoratedTree st
( t = <*T1,T2*> . i & <*(T1 . {}),(T2 . {})*> . i = t . {} ) ; :: thesis: verum

end;

hence roots <*T1,T2*> = <*(T1 . {}),(T2 . {})*> by A7, A8, TREES_3:def 18; :: thesis: verum