let S be non empty non void ManySortedSign ; :: thesis:
let s be SortSymbol of S; :: thesis:
let Z be non-trivial ManySortedSet of the carrier of S; :: thesis:
let z be Element of Z . s; :: thesis:
let C9 be context of z; :: thesis:
defpred S₁[ Element of (Free (S,Z))] means TranslationRel S reduces s, the_sort_of $1;
the_sort_of (z -term) = s by SORT;
then A1: S₁[z -term ] by REWRITE1:12;

A2: now :: thesis:

let o be OperSymbol of S; :: thesis:
let k be Element of Args (o,(Free (S,Z))); :: thesis:
assume A3: k is z -context_including ; :: thesis:
assume A4: S₁[z -context_in k] ; :: thesis:
let C be context of z; :: thesis:
assume AA: C = o -term k ; :: thesis:
thus S₁[C] :: thesis:

proof

set t = o -term k;

now :: thesis:

take o = o; :: thesis:
thus the_result_sort_of o = the_sort_of (o -term k) by Th8; :: thesis:
reconsider i = z -context_pos_in k as Element of NAT by ORDINAL1:def 12;
take i = i; :: thesis:
A7: dom k = dom (the_arity_of o) by MSUALG_3:6;
hence i in dom (the_arity_of o) by A3, Th71; :: thesis:
( k . i in the Sorts of (Free (S,Z)) . ((the_arity_of o) /. i) & k . i = z -context_in k ) by A3, A7, Th71, MSUALG_6:2;
hence (the_arity_of o) /. i = the_sort_of (z -context_in k) by SORT; :: thesis:

end;

then [(the_sort_of (z -context_in k)),(the_sort_of (o -term k))] in TranslationRel S by MSUALG_6:def 3;
then TranslationRel S reduces the_sort_of (z -context_in k), the_sort_of (o -term k) by REWRITE1:15;
hence S₁[C] by A4, AA, REWRITE1:16; :: thesis:

end;

end;

thus S₁[C9] from MSAFREE5:sch 4(A1, A2); :: thesis: