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:9;
A8: [o,the carrier of F₁()] = Sym o,(the Sorts of F₂() \/ F₃()) by MSAFREE:def 11;
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 9;
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