A4: now

let s be SortSymbol of F₁(); :: thesis: for x being Element of the Sorts of F₂() . s holds P₁[ root-tree [x,s]]
let x be Element of the Sorts of F₂() . s; :: thesis: P₁[ root-tree [x,s]]
P₁[x -term F₂(),F₃()] by A1;
hence P₁[ root-tree [x,s]] ; :: thesis: verum

end;

A5: now

let s be SortSymbol of F₁(); :: thesis: for v being Element of F₃() . s holds P₁[ root-tree [v,s]]
let v be Element of F₃() . s; :: thesis: P₁[ root-tree [v,s]]
P₁[v -term F₂()] by A2;
hence P₁[ root-tree [v,s]] ; :: thesis: verum

end;

A6: for o being OperSymbol of F₁()
for p being ArgumentSeq of Sym o,(the Sorts of F₂() \/ F₃()) st ( for t being c-Term of F₂(),F₃() st t in rng p holds
P₁[t] ) holds
P₁[(Sym o,(the Sorts of F₂() \/ F₃())) -tree p] by A3;
for t being c-Term of F₂(),F₃() holds P₁[t] from MSATERM:sch 2(A4, A5, A6);
hence for t being c-Term of F₂(),F₃() holds P₁[t] ; :: thesis: verum