set X = F2();
set G = DTConMSA F2();
A3: for nt being Symbol of (DTConMSA F2())
for ts being FinSequence of TS (DTConMSA F2()) st nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConMSA F2()) st t in rng ts holds
P1[t] ) holds
P1[nt -tree ts]
proof
let nt be Symbol of (DTConMSA F2()); :: thesis: for ts being FinSequence of TS (DTConMSA F2()) st nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConMSA F2()) st t in rng ts holds
P1[t] ) holds
P1[nt -tree ts]
let ts be FinSequence of TS (DTConMSA F2()); :: thesis: ( nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConMSA F2()) st t in rng ts holds
P1[t] ) implies P1[nt -tree ts] )
assume that
A4: nt ==> roots ts and
A5: for t being DecoratedTree of the carrier of (DTConMSA F2()) st t in rng ts holds
P1[t] ; :: thesis: P1[nt -tree ts]
nt in { s where s is Symbol of (DTConMSA F2()) : ex n being FinSequence st s ==> n } by A4;
then reconsider sy = nt as NonTerminal of (DTConMSA F2()) by LANG1:def 3;
reconsider p = ts as FinSequence of F1() -Terms F2() ;
sy in [: the carrier' of F1(),{ the carrier of F1()}:] by Lm5;
then consider o being OperSymbol of F1(), x2 being Element of { the carrier of F1()} such that
A6: sy = [o,x2] by DOMAIN_1:1;
A7: x2 = the carrier of F1() by TARSKI:def 1;
[o, the carrier of F1()] = Sym (o,F2()) by MSAFREE:def 9;
then ts is SubtreeSeq of Sym (o,F2()) by A4, A6, A7, DTCONSTR:def 6;
then reconsider p = p as ArgumentSeq of Sym (o,F2()) by Def2;
for t being Term of F1(),F2() st t in rng p holds
P1[t] by A5;
hence P1[nt -tree ts] by A2, A6, A7; :: thesis: verum
end;
A8: for s being Symbol of (DTConMSA F2()) st s in Terminals (DTConMSA F2()) holds
P1[ root-tree s]
proof
let x be Symbol of (DTConMSA F2()); :: thesis: ( x in Terminals (DTConMSA F2()) implies P1[ root-tree x] )
assume x in Terminals (DTConMSA F2()) ; :: thesis: P1[ root-tree x]
then ex s being SortSymbol of F1() ex v being Element of F2() . s st x = [v,s] by Lm3;
hence P1[ root-tree x] by A1; :: thesis: verum
end;
for t being DecoratedTree of the carrier of (DTConMSA F2()) st t in TS (DTConMSA F2()) holds
P1[t] from DTCONSTR:sch 7(A8, A3);
 hence for t being Term of F1(),F2() holds P1[t] ; :: thesis: verum