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

now

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:4, TARSKI:def 2;
hence ex t being DecoratedTree st
( t = <*T1,T2*> . i & <*(T1 . {} ),(T2 . {} )*> . i = t . {} ) by A1; :: thesis: verum

end;

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