defpred S₁[ Element of (Free (S,X))] means ($1,[x,s]) <- t is Element of the Sorts of (Free (S,X)) . (the_sort_of $1);
( ((x -term),[x,s]) <- t = t & the_sort_of (x -term) = s ) by SORT;
then A0: S₁[x -term ] by A, SORT;
A1: 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]
deffunc H₁( Nat) -> set = ((p /. $1),[x,s]) <- t;
consider q being FinSequence such that
A4: ( len q = len p & ( for i being Nat st i in dom q holds
q . i = H₁(i) ) ) from FINSEQ_1:sch 2();
A5: ( dom q = dom p & dom p <> {} ) by A2, A4, FINSEQ_3:29;
A6: ( not p is empty & not q is empty ) by A2, A4;
A8: dom p = dom (the_arity_of o) by MSUALG_6:2;
then A9: len q = len (the_arity_of o) by A4, FINSEQ_3:29;

now :: thesis: for i being Nat st i in dom q holds
q . i in the Sorts of (Free (S,X)) . ((the_arity_of o) /. i)

let i be Nat; :: thesis: ( i in dom q implies q . b₁ in the Sorts of (Free (S,X)) . ((the_arity_of o) /. b₁) )
assume B1: i in dom q ; :: thesis: q . b₁ in the Sorts of (Free (S,X)) . ((the_arity_of o) /. b₁)
then B2: p /. i = p . i by A5, 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: q . b₁ in the Sorts of (Free (S,X)) . ((the_arity_of o) /. b₁)

then B3: ( x -context_in p = p . i & q . i = H₁(i) ) by B1, A4, A2, Th71;
p . i in the Sorts of (Free (S,X)) . ((the_arity_of o) /. i) by B1, A5, A8, MSUALG_6:2;
then the_sort_of (x -context_in p) = (the_arity_of o) /. i by B3, SORT;
hence q . i in the Sorts of (Free (S,X)) . ((the_arity_of o) /. i) by B2, B3, A3; :: thesis: verum

end;

suppose x -context_pos_in p <> i ; :: thesis: q . b₁ in the Sorts of (Free (S,X)) . ((the_arity_of o) /. b₁)

then ( q . i = H₁(i) & H₁(i) = p . i ) by A4, B1, B2, A2, A5, Th72, Th23;
hence q . i in the Sorts of (Free (S,X)) . ((the_arity_of o) /. i) by B1, A5, A8, MSUALG_6:2; :: thesis: verum

end;

end;

end;

then reconsider q = q as Element of Args (o,(Free (S,X))) by A9, MSAFREE2:5;

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

let i be Nat; :: thesis: for d1 being DecoratedTree st i in dom p & d1 = p . i holds
q . i = (d1,[x,s]) <- t
let d1 be DecoratedTree; :: thesis: ( i in dom p & d1 = p . i implies q . i = (d1,[x,s]) <- t )
assume ( i in dom p & d1 = p . i ) ; :: thesis: q . i = (d1,[x,s]) <- t
then ( q . i = H₁(i) & p /. i = d1 ) by A4, A5, PARTFUN1:def 6;
hence q . i = (d1,[x,s]) <- t ; :: thesis: verum

end;

then ((o -term p),[x,s]) <- t = o -term q by A6, ThL8, A4, FINSEQ_3:29;
hence for C being context of x st C = o -term p holds
S₁[C] by Th8; :: thesis: verum

end;

thus S₁[C] from MSAFREE5:sch 4(A0, A1); :: thesis: verum