let T1, T2 be DecoratedTree; 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 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 ;
( 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*>
;
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;
verum end;
hence
roots <*T1,T2*> = <*(T1 . {}),(T2 . {})*>
by A7, A8, TREES_3:def 18; verum