defpred S₁[ Element of (Free (S,X))] means ($1,[x,s]) <- (x -term) = $1;
A1: S₁[x -term ] ;
A2: for o being OperSymbol of S
for p being Element of Args (o,(Free (S,X))) st p is x -context_including & S₁[x -context_in p] holds
for C being context of x st C = o -term p holds
S₁[C]

proof

let o be OperSymbol of S; :: thesis: for p being Element of Args (o,(Free (S,X))) st p is x -context_including & S₁[x -context_in p] holds
for C being context of x st C = o -term p holds
S₁[C]
let p be Element of Args (o,(Free (S,X))); :: thesis: ( p is x -context_including & S₁[x -context_in p] implies for C being context of x st C = o -term p holds
S₁[C] )
assume that
A2: p is x -context_including and
A3: S₁[x -context_in p] ; :: thesis: for C being context of x st C = o -term p holds
S₁[C]
set t = x -term ;
deffunc H₁( Nat) -> set = ((p /. $1),[x,s]) <- (x -term);

now :: thesis: for i being Nat
for d1 being DecoratedTree st i in dom p & d1 = p . i holds
p . i = (d1,[x,s]) <- (x -term)

let i be Nat; :: thesis: for d1 being DecoratedTree st i in dom p & d1 = p . i holds
p . b₂ = (b₃,[x,s]) <- (x -term)
let d1 be DecoratedTree; :: thesis: ( i in dom p & d1 = p . i implies p . b₁ = (b₂,[x,s]) <- (x -term) )
assume B1: ( i in dom p & d1 = p . i ) ; :: thesis: p . b₁ = (b₂,[x,s]) <- (x -term)
then B2: p /. i = d1 by PARTFUN1:def 6;

per cases ( x -context_pos_in p = i or x -context_pos_in p <> i ) ;

suppose x -context_pos_in p = i ; :: thesis: p . b₁ = (b₂,[x,s]) <- (x -term)

then x -context_in p = p . i by A2, Th71;
hence p . i = (d1,[x,s]) <- (x -term) by A3, B1; :: thesis: verum

end;

suppose x -context_pos_in p <> i ; :: thesis: p . b₁ = (b₂,[x,s]) <- (x -term)

hence p . i = (d1,[x,s]) <- (x -term) by B1, B2, A2, Th72, Th23; :: thesis: verum

end;

end;

end;

hence for C being context of x st C = o -term p holds
S₁[C] by A2, ThL8; :: thesis: verum

end;

AA: S₁[C] from MSAFREE5:sch 4(A1, A2);
the_sort_of (x -term) = s by SORT;
hence C -sub (x -term) = C by AA, SUB; :: thesis: verum