let term be bin-term; :: thesis: ( ex t being Terminal of SCM-AE st term = root-tree t or ex tl, tr being bin-term st
( term = tl + tr or term = tl - tr or term = tl * tr or term = tl div tr or term = tl mod tr ) )
root-label term in the carrier of SCM-AE ;
then term . {} in the carrier of SCM-AE by BINTREE1:def 1;
then A1: term . {} in (Terminals SCM-AE ) \/ (NonTerminals SCM-AE ) by LANG1:1;

per cases ( term . {} in Terminals SCM-AE or term . {} in NonTerminals SCM-AE ) by A1, XBOOLE_0:def 3;

suppose term . {} in Terminals SCM-AE ; :: thesis: ( ex t being Terminal of SCM-AE st term = root-tree t or ex tl, tr being bin-term st
( term = tl + tr or term = tl - tr or term = tl * tr or term = tl div tr or term = tl mod tr ) )

then reconsider t = term . {} as Terminal of SCM-AE ;
term = root-tree t by DTCONSTR:9;
hence ( ex t being Terminal of SCM-AE st term = root-tree t or ex tl, tr being bin-term st
( term = tl + tr or term = tl - tr or term = tl * tr or term = tl div tr or term = tl mod tr ) ) ; :: thesis: verum

end;

suppose term . {} in NonTerminals SCM-AE ; :: thesis: ( ex t being Terminal of SCM-AE st term = root-tree t or ex tl, tr being bin-term st
( term = tl + tr or term = tl - tr or term = tl * tr or term = tl div tr or term = tl mod tr ) )

then reconsider nt = term . {} as NonTerminal of SCM-AE ;
consider ts being FinSequence of TS SCM-AE such that
A2: ( term = nt -tree ts & nt ==> roots ts ) by DTCONSTR:10;
consider x1, x2 being Symbol of SCM-AE such that
A3: roots ts = <*x1,x2*> by A2, BINTREE1:def 4;
A4: ( dom (roots ts) = dom ts & ( for i being Element of NAT st i in dom ts holds
ex T being DecoratedTree st
( T = ts . i & (roots ts) . i = T . {} ) ) ) by TREES_3:def 18;
len (roots ts) = 2 by A3, FINSEQ_1:61;
then A5: dom (roots ts) = Seg 2 by FINSEQ_1:def 3;
then A6: len ts = 2 by A4, FINSEQ_1:def 3;
A7: ( 1 in Seg 2 & 2 in Seg 2 ) by FINSEQ_1:4, TARSKI:def 2;
then consider tl being DecoratedTree such that
A8: ( tl = ts . 1 & (roots ts) . 1 = tl . {} ) by A4, A5;
consider tr being DecoratedTree such that
A9: ( tr = ts . 2 & (roots ts) . 2 = tr . {} ) by A4, A5, A7;
reconsider tl = tl, tr = tr as bin-term by A4, A5, A7, A8, A9, FINSEQ_2:13;
ts = <*tl,tr*> by A6, A8, A9, FINSEQ_1:61;
then term = nt -tree tl,tr by A2, TREES_4:def 6;
then ( term = tl + tr or term = tl - tr or term = tl * tr or term = tl div tr or term = tl mod tr ) by Th3;
hence ( ex t being Terminal of SCM-AE st term = root-tree t or ex tl, tr being bin-term st
( term = tl + tr or term = tl - tr or term = tl * tr or term = tl div tr or term = tl mod tr ) ) ; :: thesis: verum

end;

end;