defpred S₁[ Element of (Free (F₁(),F₃()))] means ( $1 is context of F₄() implies P₁[$1] );
A2: for s being SortSymbol of F₁()
for x being Element of F₃() . s holds S₁[x -term ]

proof

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 ]
assume x -term is context of F₄() ; :: thesis: P₁[x -term ]
then ( s = F₂() & x = F₄() ) by Th27;
hence P₁[x -term ] by A0; :: thesis: verum

end;

A3: 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]

proof

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 that
A4: for t being Element of (Free (F₁(),F₃())) st t in rng p holds
S₁[t] and
A5: o -term p is context of F₄() ; :: thesis: P₁[o -term p]
p is F₄() -context_including by A5, Th53;
then F₄() -context_in p in rng p by CIn;
then P₁[F₄() -context_in p] by A4;
hence P₁[o -term p] by A1, A5, Th53; :: thesis: verum

end;

S₁[F₅()] from MSAFREE5:sch 2(A2, A3);
hence P₁[F₅()] ; :: thesis: verum