let G be non empty with_terminals with_nonterminals binary DTConstrStr ; :: thesis: for ts being FinSequence of TS G

for nt being Symbol of G st nt ==> roots ts holds

( nt is NonTerminal of G & dom ts = {1,2} & 1 in dom ts & 2 in dom ts & ex tl, tr being Element of TS G st

( roots ts = <*(root-label tl),(root-label tr)*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts ) )

let ts be FinSequence of TS G; :: thesis: for nt being Symbol of G st nt ==> roots ts holds

( nt is NonTerminal of G & dom ts = {1,2} & 1 in dom ts & 2 in dom ts & ex tl, tr being Element of TS G st

( roots ts = <*(root-label tl),(root-label tr)*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts ) )

let nt be Symbol of G; :: thesis: ( nt ==> roots ts implies ( nt is NonTerminal of G & dom ts = {1,2} & 1 in dom ts & 2 in dom ts & ex tl, tr being Element of TS G st

( roots ts = <*(root-label tl),(root-label tr)*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts ) ) )

assume A1: nt ==> roots ts ; :: thesis: ( nt is NonTerminal of G & dom ts = {1,2} & 1 in dom ts & 2 in dom ts & ex tl, tr being Element of TS G st

( roots ts = <*(root-label tl),(root-label tr)*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts ) )

then consider rtl, rtr being Symbol of G such that

A2: roots ts = <*rtl,rtr*> by Def4;

nt in { s where s is Symbol of G : ex rts being FinSequence st s ==> rts } by A1;

hence nt is NonTerminal of G by LANG1:def 3; :: thesis: ( dom ts = {1,2} & 1 in dom ts & 2 in dom ts & ex tl, tr being Element of TS G st

( roots ts = <*(root-label tl),(root-label tr)*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts ) )

A3: len <*rtl,rtr*> = 2 by FINSEQ_1:44;

A4: dom <*rtl,rtr*> = dom ts by A2, TREES_3:def 18;

hence dom ts = {1,2} by A3, FINSEQ_1:2, FINSEQ_1:def 3; :: thesis: ( 1 in dom ts & 2 in dom ts & ex tl, tr being Element of TS G st

( roots ts = <*(root-label tl),(root-label tr)*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts ) )

hence A5: ( 1 in dom ts & 2 in dom ts ) by TARSKI:def 2; :: thesis: ex tl, tr being Element of TS G st

( roots ts = <*(root-label tl),(root-label tr)*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts )

then consider tl being DecoratedTree such that

A6: tl = ts . 1 and

A7: <*rtl,rtr*> . 1 = tl . {} by A2, TREES_3:def 18;

A8: ( rng ts c= TS G & tl in rng ts ) by A5, A6, FINSEQ_1:def 4, FUNCT_1:def 3;

consider tr being DecoratedTree such that

A9: tr = ts . 2 and

A10: <*rtl,rtr*> . 2 = tr . {} by A2, A5, TREES_3:def 18;

tr in rng ts by A5, A9, FUNCT_1:def 3;

then reconsider tl = tl, tr = tr as Element of TS G by A8;

take tl ; :: thesis: ex tr being Element of TS G st

( roots ts = <*(root-label tl),(root-label tr)*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts )

take tr ; :: thesis: ( roots ts = <*(root-label tl),(root-label tr)*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts )

<*rtl,rtr*> . 1 = rtl by FINSEQ_1:44;

hence roots ts = <*(root-label tl),(root-label tr)*> by A2, A7, A10, FINSEQ_1:44; :: thesis: ( tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts )

Seg (len <*rtl,rtr*>) = dom <*rtl,rtr*> by FINSEQ_1:def 3

.= Seg (len ts) by A4, FINSEQ_1:def 3 ;

then len ts = 2 by A3, FINSEQ_1:6;

then ts = <*tl,tr*> by A6, A9, FINSEQ_1:44;

hence ( tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) ) by A6, A9, TREES_4:def 6; :: thesis: ( tl in rng ts & tr in rng ts )

thus ( tl in rng ts & tr in rng ts ) by A5, A6, A9, FUNCT_1:def 3; :: thesis: verum

for nt being Symbol of G st nt ==> roots ts holds

( nt is NonTerminal of G & dom ts = {1,2} & 1 in dom ts & 2 in dom ts & ex tl, tr being Element of TS G st

( roots ts = <*(root-label tl),(root-label tr)*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts ) )

let ts be FinSequence of TS G; :: thesis: for nt being Symbol of G st nt ==> roots ts holds

( nt is NonTerminal of G & dom ts = {1,2} & 1 in dom ts & 2 in dom ts & ex tl, tr being Element of TS G st

( roots ts = <*(root-label tl),(root-label tr)*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts ) )

let nt be Symbol of G; :: thesis: ( nt ==> roots ts implies ( nt is NonTerminal of G & dom ts = {1,2} & 1 in dom ts & 2 in dom ts & ex tl, tr being Element of TS G st

( roots ts = <*(root-label tl),(root-label tr)*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts ) ) )

assume A1: nt ==> roots ts ; :: thesis: ( nt is NonTerminal of G & dom ts = {1,2} & 1 in dom ts & 2 in dom ts & ex tl, tr being Element of TS G st

( roots ts = <*(root-label tl),(root-label tr)*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts ) )

then consider rtl, rtr being Symbol of G such that

A2: roots ts = <*rtl,rtr*> by Def4;

nt in { s where s is Symbol of G : ex rts being FinSequence st s ==> rts } by A1;

hence nt is NonTerminal of G by LANG1:def 3; :: thesis: ( dom ts = {1,2} & 1 in dom ts & 2 in dom ts & ex tl, tr being Element of TS G st

( roots ts = <*(root-label tl),(root-label tr)*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts ) )

A3: len <*rtl,rtr*> = 2 by FINSEQ_1:44;

A4: dom <*rtl,rtr*> = dom ts by A2, TREES_3:def 18;

hence dom ts = {1,2} by A3, FINSEQ_1:2, FINSEQ_1:def 3; :: thesis: ( 1 in dom ts & 2 in dom ts & ex tl, tr being Element of TS G st

( roots ts = <*(root-label tl),(root-label tr)*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts ) )

hence A5: ( 1 in dom ts & 2 in dom ts ) by TARSKI:def 2; :: thesis: ex tl, tr being Element of TS G st

( roots ts = <*(root-label tl),(root-label tr)*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts )

then consider tl being DecoratedTree such that

A6: tl = ts . 1 and

A7: <*rtl,rtr*> . 1 = tl . {} by A2, TREES_3:def 18;

A8: ( rng ts c= TS G & tl in rng ts ) by A5, A6, FINSEQ_1:def 4, FUNCT_1:def 3;

consider tr being DecoratedTree such that

A9: tr = ts . 2 and

A10: <*rtl,rtr*> . 2 = tr . {} by A2, A5, TREES_3:def 18;

tr in rng ts by A5, A9, FUNCT_1:def 3;

then reconsider tl = tl, tr = tr as Element of TS G by A8;

take tl ; :: thesis: ex tr being Element of TS G st

( roots ts = <*(root-label tl),(root-label tr)*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts )

take tr ; :: thesis: ( roots ts = <*(root-label tl),(root-label tr)*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts )

<*rtl,rtr*> . 1 = rtl by FINSEQ_1:44;

hence roots ts = <*(root-label tl),(root-label tr)*> by A2, A7, A10, FINSEQ_1:44; :: thesis: ( tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts )

Seg (len <*rtl,rtr*>) = dom <*rtl,rtr*> by FINSEQ_1:def 3

.= Seg (len ts) by A4, FINSEQ_1:def 3 ;

then len ts = 2 by A3, FINSEQ_1:6;

then ts = <*tl,tr*> by A6, A9, FINSEQ_1:44;

hence ( tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) ) by A6, A9, TREES_4:def 6; :: thesis: ( tl in rng ts & tr in rng ts )

thus ( tl in rng ts & tr in rng ts ) by A5, A6, A9, FUNCT_1:def 3; :: thesis: verum