let G be non empty with_terminals DTConstrStr ; :: thesis: for tsg being Element of TS G
for s being Terminal of G st tsg . {} = s holds
tsg = root-tree s
let tsg be Element of TS G; :: thesis: for s being Terminal of G st tsg . {} = s holds
tsg = root-tree s
let s be Terminal of G; :: thesis: ( tsg . {} = s implies tsg = root-tree s )
assume A1: tsg . {} = s ; :: thesis: tsg = root-tree s
defpred S2[ DecoratedTree of the carrier of G] means for s being Terminal of G st $1 . {} = s holds
$1 = root-tree s;
A2: for s being Symbol of G st s in Terminals G holds
S2[ root-tree s] by TREES_4:3;
A3: now :: thesis: for nt being Symbol of G
for ts being FinSequence of TS G st nt ==> roots ts & ( for t being DecoratedTree of the carrier of G st t in rng ts holds
S2[t] ) holds
S2[nt -tree ts]
let nt be Symbol of G; :: thesis: for ts being FinSequence of TS G st nt ==> roots ts & ( for t being DecoratedTree of the carrier of G st t in rng ts holds
S2[t] ) holds
S2[nt -tree ts]
let ts be FinSequence of TS G; :: thesis: ( nt ==> roots ts & ( for t being DecoratedTree of the carrier of G st t in rng ts holds
S2[t] ) implies S2[nt -tree ts] )
assume that
A4: nt ==> roots ts and
for t being DecoratedTree of the carrier of G st t in rng ts holds
S2[t] ; :: thesis: S2[nt -tree ts]
thus S2[nt -tree ts] :: thesis: verum
proof
let s be Terminal of G; :: thesis: ( (nt -tree ts) . {} = s implies nt -tree ts = root-tree s )
assume A5: (nt -tree ts) . {} = s ; :: thesis: nt -tree ts = root-tree s
A6: (nt -tree ts) . {} = nt by TREES_4:def 4;
A7: s in Terminals G ;
Terminals G = { t where t is Symbol of G : for tnt being FinSequence holds not t ==> tnt } by LANG1:def 2;
then ex t being Symbol of G st
( s = t & ( for tnt being FinSequence holds not t ==> tnt ) ) by A7;
hence nt -tree ts = root-tree s by A4, A5, A6; :: thesis: verum
end;
end;
for t being DecoratedTree of the carrier of G st t in TS G holds
S2[t] from DTCONSTR:sch 7(A2, A3);
 hence tsg = root-tree s by A1; :: thesis: verum