set X = the Sorts of F₂() (\/) F₃();
set G = DTConMSA ( the Sorts of F₂() (\/) F₃());
A4: for nt being Symbol of (DTConMSA ( the Sorts of F₂() (\/) F₃()))
for ts being FinSequence of TS (DTConMSA ( the Sorts of F₂() (\/) F₃())) st nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConMSA ( the Sorts of F₂() (\/) F₃())) st t in rng ts holds
P₁[t] ) holds
P₁[nt -tree ts]

proof

let nt be Symbol of (DTConMSA ( the Sorts of F₂() (\/) F₃())); :: thesis: for ts being FinSequence of TS (DTConMSA ( the Sorts of F₂() (\/) F₃())) st nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConMSA ( the Sorts of F₂() (\/) F₃())) st t in rng ts holds
P₁[t] ) holds
P₁[nt -tree ts]
let ts be FinSequence of TS (DTConMSA ( the Sorts of F₂() (\/) F₃())); :: thesis: ( nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConMSA ( the Sorts of F₂() (\/) F₃())) st t in rng ts holds
P₁[t] ) implies P₁[nt -tree ts] )
assume that
A5: nt ==> roots ts and
A6: for t being DecoratedTree of the carrier of (DTConMSA ( the Sorts of F₂() (\/) F₃())) st t in rng ts holds
P₁[t] ; :: thesis: P₁[nt -tree ts]
nt in { s where s is Symbol of (DTConMSA ( the Sorts of F₂() (\/) F₃())) : ex n being FinSequence st s ==> n } by A5;
then reconsider sy = nt as NonTerminal of (DTConMSA ( the Sorts of F₂() (\/) F₃())) by LANG1:def 3;
reconsider p = ts as FinSequence of F₁() -Terms ( the Sorts of F₂() (\/) F₃()) ;
sy in [: the carrier' of F₁(),{ the carrier of F₁()}:] by Lm5;
then consider o being OperSymbol of F₁(), x2 being Element of { the carrier of F₁()} such that
A7: sy = [o,x2] by DOMAIN_1:1;
A8: [o, the carrier of F₁()] = Sym (o,( the Sorts of F₂() (\/) F₃())) by MSAFREE:def 9;
A9: x2 = the carrier of F₁() by TARSKI:def 1;
then ts is SubtreeSeq of Sym (o,( the Sorts of F₂() (\/) F₃())) by A5, A7, A8, DTCONSTR:def 6;
then reconsider p = p as ArgumentSeq of Sym (o,( the Sorts of F₂() (\/) F₃())) by Def2;
for t being c-Term of F₂(),F₃() st t in rng p holds
P₁[t] by A6;
hence P₁[nt -tree ts] by A3, A7, A9, A8; :: thesis: verum

end;

A10: for s being Symbol of (DTConMSA ( the Sorts of F₂() (\/) F₃())) st s in Terminals (DTConMSA ( the Sorts of F₂() (\/) F₃())) holds
P₁[ root-tree s]

proof

let x be Symbol of (DTConMSA ( the Sorts of F₂() (\/) F₃())); :: thesis: ( x in Terminals (DTConMSA ( the Sorts of F₂() (\/) F₃())) implies P₁[ root-tree x] )
assume x in Terminals (DTConMSA ( the Sorts of F₂() (\/) F₃())) ; :: thesis: P₁[ root-tree x]
then ( ex s being SortSymbol of F₁() ex a being set st
( a in the Sorts of F₂() . s & x = [a,s] ) or ex s being SortSymbol of F₁() ex v being Element of F₃() . s st x = [v,s] ) by Lm4;
hence P₁[ root-tree x] by A1, A2; :: thesis: verum

end;

for t being DecoratedTree of the carrier of (DTConMSA ( the Sorts of F₂() (\/) F₃())) st t in TS (DTConMSA ( the Sorts of F₂() (\/) F₃())) holds
P₁[t] from DTCONSTR:sch 7(A10, A4);
hence for t being c-Term of F₂(),F₃() holds P₁[t] ; :: thesis: verum