let G, G' be non empty DTConstrStr ; :: thesis: ( Terminals G c= Terminals G' & the Rules of G c= the Rules of G' implies TS G c= TS G' )
assume that
Z0: Terminals G c= Terminals G' and
Z1: the Rules of G c= the Rules of G' ; :: thesis: TS G c= TS G'
Z2: ( the carrier of G' = (Terminals G') \/ (NonTerminals G') & the carrier of G c= the carrier of G' ) by Z0, Z1, LemTerm0, LANG1:1;
defpred S₁[ set ] means $1 in TS G';
A1: for s being Symbol of G st s in Terminals G holds
S₁[ root-tree s]

proof

let s be Symbol of G; :: thesis: ( s in Terminals G implies S₁[ root-tree s] )
assume 00: s in Terminals G ; :: thesis: S₁[ root-tree s]
then reconsider s' = s as Symbol of G' by Z0, Z2, XBOOLE_0:def 3;
root-tree s = root-tree s' ;
hence S₁[ root-tree s] by 00, Z0, DTCONSTR:def 4; :: thesis: verum

end;

A2: for nt being Symbol of G
for ts being FinSequence of TS G st nt ==> roots ts & ( for t being DecoratedTree of st t in rng ts holds
S₁[t] ) holds
S₁[nt -tree ts]

proof

let n be Symbol of G; :: thesis: for ts being FinSequence of TS G st n ==> roots ts & ( for t being DecoratedTree of st t in rng ts holds
S₁[t] ) holds
S₁[n -tree ts]
let s be FinSequence of TS G; :: thesis: ( n ==> roots s & ( for t being DecoratedTree of st t in rng s holds
S₁[t] ) implies S₁[n -tree s] )
assume that
01: [n,(roots s)] in the Rules of G and
02: for t being DecoratedTree of st t in rng s holds
S₁[t] ; :: according to LANG1:def 1 :: thesis: S₁[n -tree s]
rng s c= TS G'

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng s or x in TS G' )
assume 03: x in rng s ; :: thesis: x in TS G'
then x is DecoratedTree of by TREES_3:def 6;
hence x in TS G' by 02, 03; :: thesis: verum

end;

then reconsider s' = s as FinSequence of TS G' by FINSEQ_1:def 4;
n in the carrier of G ;
then reconsider n' = n as Symbol of G' by Z2;
n' ==> roots s' by Z1, 01, LANG1:def 1;
hence S₁[n -tree s] by DTCONSTR:def 4; :: thesis: verum

end;

A3: for t being DecoratedTree of st t in TS G holds
S₁[t] from DTCONSTR:sch 7(A1, A2);
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in TS G or x in TS G' )
assume A4: x in TS G ; :: thesis: x in TS G'
then reconsider t = x as Element of FinTrees the carrier of G ;
S₁[t] by A3, A4;
hence x in TS G' ; :: thesis: verum