AA: F3() is Term of F1(),F2() by MSAFREE4:42;
A3: now :: thesis: for s being SortSymbol of F1()
for x being Element of F2() . s holds P1[ root-tree [x,s]]
let s be SortSymbol of F1(); :: thesis: for x being Element of F2() . s holds P1[ root-tree [x,s]]
let x be Element of F2() . s; :: thesis: P1[ root-tree [x,s]]
P1[x -term ] by A1;
hence P1[ root-tree [x,s]] ; :: thesis: verum
end;
A4: now :: thesis: for o being OperSymbol of F1()
for p being ArgumentSeq of Sym (o,F2()) st ( for t being Term of F1(),F2() st t in rng p holds
P1[t] ) holds
P1[[o, the carrier of F1()] -tree p]
let o be OperSymbol of F1(); :: thesis: for p being ArgumentSeq of Sym (o,F2()) st ( for t being Term of F1(),F2() st t in rng p holds
P1[t] ) holds
P1[[o, the carrier of F1()] -tree p]
let p be ArgumentSeq of Sym (o,F2()); :: thesis: ( ( for t being Term of F1(),F2() st t in rng p holds
P1[t] ) implies P1[[o, the carrier of F1()] -tree p] )
Free (F1(),F2()) = FreeMSA F2() by MSAFREE3:31;
then reconsider q = p as Element of Args (o,(Free (F1(),F2()))) by INSTALG1:1;
assume A5: for t being Term of F1(),F2() st t in rng p holds
P1[t] ; :: thesis: P1[[o, the carrier of F1()] -tree p]
now :: thesis: for u being Element of (Free (F1(),F2())) st u in rng q holds
P1[u]
let u be Element of (Free (F1(),F2())); :: thesis: ( u in rng q implies P1[u] )
u is Term of F1(),F2() by MSAFREE4:42;
hence ( u in rng q implies P1[u] ) by A5; :: thesis: verum
end;
then P1[o -term q] by A2;
hence P1[[o, the carrier of F1()] -tree p] ; :: thesis: verum
end;
for t being Term of F1(),F2() holds P1[t] from MSATERM:sch 1(A3, A4);
 hence P1[F3()] by AA; :: thesis: verum