A4: now :: thesis: for s being SortSymbol of F1()
for x being Element of the Sorts of F2() . s holds P1[ root-tree [x,s]]
let s be SortSymbol of F1(); :: thesis: for x being Element of the Sorts of F2() . s holds P1[ root-tree [x,s]]
let x be Element of the Sorts of F2() . s; :: thesis: P1[ root-tree [x,s]]
P1[x -term (F2(),F3())] by A1;
hence P1[ root-tree [x,s]] ; :: thesis: verum
end;
A5: now :: thesis: for s being SortSymbol of F1()
for v being Element of F3() . s holds P1[ root-tree [v,s]]
let s be SortSymbol of F1(); :: thesis: for v being Element of F3() . s holds P1[ root-tree [v,s]]
let v be Element of F3() . s; :: thesis: P1[ root-tree [v,s]]
P1[v -term F2()] by A2;
hence P1[ root-tree [v,s]] ; :: thesis: verum
end;
A6: for o being OperSymbol of F1()
for p being ArgumentSeq of Sym (o,( the Sorts of F2() (\/) F3())) st ( for t being c-Term of F2(),F3() st t in rng p holds
P1[t] ) holds
P1[(Sym (o,( the Sorts of F2() (\/) F3()))) -tree p] by A3;
for t being c-Term of F2(),F3() holds P1[t] from MSATERM:sch 2(A4, A5, A6);
 hence for t being c-Term of F2(),F3() holds P1[t] ; :: thesis: verum