AA:
F3() is Term of F1(),F2()
by MSAFREE4:42;
A4:
now 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();
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());
( ( 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]
;
P1[[o, the carrier of F1()] -tree p]then
P1[
o -term q]
by A2;
hence
P1[
[o, the carrier of F1()] -tree p]
;
verum end;
for t being Term of F1(),F2() holds P1[t]
from MSATERM:sch 1(A3, A4);
hence
P1[F3()]
by AA; verum