let S be non empty non void ManySortedSign ; :: thesis: for s being SortSymbol of S
for Z being non-trivial ManySortedSet of the carrier of S
for z being Element of Z . s
for C9 being context of z holds TranslationRel S reduces s, the_sort_of C9
let s be SortSymbol of S; :: thesis: for Z being non-trivial ManySortedSet of the carrier of S
for z being Element of Z . s
for C9 being context of z holds TranslationRel S reduces s, the_sort_of C9
let Z be non-trivial ManySortedSet of the carrier of S; :: thesis: for z being Element of Z . s
for C9 being context of z holds TranslationRel S reduces s, the_sort_of C9
let z be Element of Z . s; :: thesis: for C9 being context of z holds TranslationRel S reduces s, the_sort_of C9
let C9 be context of z; :: thesis: TranslationRel S reduces s, the_sort_of C9
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: for o being OperSymbol of S
for k being Element of Args (o,(Free (S,Z))) st k is z -context_including & S₁[z -context_in k] holds
for C being context of z st C = o -term k holds
S₁[C]

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

proof

set t = o -term k;

now :: thesis: ex o being OperSymbol of S st
( the_result_sort_of o = the_sort_of (o -term k) & ex i being Element of NAT st
( i in dom (the_arity_of o) & (the_arity_of o) /. i = the_sort_of (z -context_in k) ) )

take o = o; :: thesis: ( the_result_sort_of o = the_sort_of (o -term k) & ex i being Element of NAT st
( i in dom (the_arity_of o) & (the_arity_of o) /. i = the_sort_of (z -context_in k) ) )
thus the_result_sort_of o = the_sort_of (o -term k) by Th8; :: thesis: ex i being Element of NAT st
( i in dom (the_arity_of o) & (the_arity_of o) /. i = the_sort_of (z -context_in k) )
reconsider i = z -context_pos_in k as Element of NAT by ORDINAL1:def 12;
take i = i; :: thesis: ( i in dom (the_arity_of o) & (the_arity_of o) /. i = the_sort_of (z -context_in k) )
A7: dom k = dom (the_arity_of o) by MSUALG_3:6;
hence i in dom (the_arity_of o) by A3, Th71; :: thesis: (the_arity_of o) /. i = the_sort_of (z -context_in k)
( 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: verum

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: verum

end;

end;

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