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;
A3: <*T1,T2*> . 1 = T1 by FINSEQ_1:44;
A4: <*(T1 . {}),(T2 . {})*> . 1 = T1 . {} by FINSEQ_1:44;
A5: <*T1,T2*> . 2 = T2 by FINSEQ_1:44;
A6: <*(T1 . {}),(T2 . {})*> . 2 = T2 . {} 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

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 . {} ) by A3, A4, A5, A6; :: thesis: verum

end;

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