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