defpred S₁[ set ] means ( $1 in F₃() implies P₁[$1] );

A3: now :: thesis: for s being SortSymbol of F₁()
for x being Element of F₂() . s holds S₁[x -term ]

let s be SortSymbol of F₁(); :: thesis: for x being Element of F₂() . s holds S₁[x -term ]
let x be Element of F₂() . s; :: thesis: S₁[x -term ]
x -term in F₃() by Th24;
hence S₁[x -term ] by A1; :: thesis: verum

end;

A4: now :: thesis: for o being OperSymbol of F₁()
for p being Element of Args (o,(Free (F₁(),F₂()))) st ( for t being Element of (Free (F₁(),F₂())) st t in rng p holds
S₁[t] ) holds
S₁[o -term p]

let o be OperSymbol of F₁(); :: thesis: for p being Element of Args (o,(Free (F₁(),F₂()))) st ( for t being Element of (Free (F₁(),F₂())) st t in rng p holds
S₁[t] ) holds
S₁[o -term p]
let p be Element of Args (o,(Free (F₁(),F₂()))); :: thesis: ( ( for t being Element of (Free (F₁(),F₂())) st t in rng p holds
S₁[t] ) implies S₁[o -term p] )
assume A5: for t being Element of (Free (F₁(),F₂())) st t in rng p holds
S₁[t] ; :: thesis: S₁[o -term p]
thus S₁[o -term p] :: thesis: verum

proof

assume A7: o -term p in F₃() ; :: thesis: P₁[o -term p]

now :: thesis: for t being Element of F₃() st t in rng p holds
P₁[t]

let t be Element of F₃(); :: thesis: ( t in rng p implies P₁[t] )
assume AA: t in rng p ; :: thesis: P₁[t]
( t in F₃() & S₁[ @ t] ) by A5, AA;
hence P₁[t] ; :: thesis: verum

end;

hence P₁[o -term p] by A2, A7; :: thesis: verum

end;

end;

S₁[ @ F₄()] from MSAFREE5:sch 2(A3, A4);
hence P₁[F₄()] by ELEM; :: thesis: verum