let S be non empty non void ManySortedSign ; :: thesis: for s1 being SortSymbol of S
for Y being infinite-yielding ManySortedSet of the carrier of S
for s2 being b₁ -reachable SortSymbol of S
for g1 being Translation of Free (S,Y),s1,s2 ex y11 being Element of Y . s1 ex C12 being context of y11 st
( the_sort_of C12 = s2 & g1 = transl C12 )
let s1 be SortSymbol of S; :: thesis: for Y being infinite-yielding ManySortedSet of the carrier of S
for s2 being s1 -reachable SortSymbol of S
for g1 being Translation of Free (S,Y),s1,s2 ex y11 being Element of Y . s1 ex C12 being context of y11 st
( the_sort_of C12 = s2 & g1 = transl C12 )
let Y be infinite-yielding ManySortedSet of the carrier of S; :: thesis: for s2 being s1 -reachable SortSymbol of S
for g1 being Translation of Free (S,Y),s1,s2 ex y11 being Element of Y . s1 ex C12 being context of y11 st
( the_sort_of C12 = s2 & g1 = transl C12 )
let s2 be s1 -reachable SortSymbol of S; :: thesis: for g1 being Translation of Free (S,Y),s1,s2 ex y11 being Element of Y . s1 ex C12 being context of y11 st
( the_sort_of C12 = s2 & g1 = transl C12 )
let g1 be Translation of Free (S,Y),s1,s2; :: thesis: ex y11 being Element of Y . s1 ex C12 being context of y11 st
( the_sort_of C12 = s2 & g1 = transl C12 )
defpred S₁[ Function, SortSymbol of S, SortSymbol of S] means for V being finite set ex x being Element of Y . $2 ex C being context of x st
( x nin V & the_sort_of C = $3 & $1 = transl C );
A1: for s being SortSymbol of S holds S₁[ id ( the Sorts of (Free (S,Y)) . s),s,s]

proof

let s be SortSymbol of S; :: thesis: S₁[ id ( the Sorts of (Free (S,Y)) . s),s,s]
let V be finite set ; :: thesis: ex x being Element of Y . s ex C being context of x st
( x nin V & the_sort_of C = s & id ( the Sorts of (Free (S,Y)) . s) = transl C )
reconsider x = the Element of (Y . s) \ V as Element of Y . s ;
reconsider C = x -term as context of x ;
take x ; :: thesis: ex C being context of x st
( x nin V & the_sort_of C = s & id ( the Sorts of (Free (S,Y)) . s) = transl C )
take C ; :: thesis: ( x nin V & the_sort_of C = s & id ( the Sorts of (Free (S,Y)) . s) = transl C )
thus x nin V by XBOOLE_0:def 5; :: thesis: ( the_sort_of C = s & id ( the Sorts of (Free (S,Y)) . s) = transl C )
thus the_sort_of C = s by SORT; :: thesis: id ( the Sorts of (Free (S,Y)) . s) = transl C
thus id ( the Sorts of (Free (S,Y)) . s) = transl C by Th57; :: thesis: verum

end;

A2: for s1, s2, s3 being SortSymbol of S st TranslationRel S reduces s1,s2 holds
for t being Translation of Free (S,Y),s1,s2 st S₁[t,s1,s2] holds
for f being Function st f is_e.translation_of Free (S,Y),s2,s3 holds
S₁[f * t,s1,s3]

proof

let s1, s2, s3 be SortSymbol of S; :: thesis: ( TranslationRel S reduces s1,s2 implies for t being Translation of Free (S,Y),s1,s2 st S₁[t,s1,s2] holds
for f being Function st f is_e.translation_of Free (S,Y),s2,s3 holds
S₁[f * t,s1,s3] )
assume TranslationRel S reduces s1,s2 ; :: thesis: for t being Translation of Free (S,Y),s1,s2 st S₁[t,s1,s2] holds
for f being Function st f is_e.translation_of Free (S,Y),s2,s3 holds
S₁[f * t,s1,s3]
let t be Translation of Free (S,Y),s1,s2; :: thesis: ( S₁[t,s1,s2] implies for f being Function st f is_e.translation_of Free (S,Y),s2,s3 holds
S₁[f * t,s1,s3] )
assume Z1: S₁[t,s1,s2] ; :: thesis: for f being Function st f is_e.translation_of Free (S,Y),s2,s3 holds
S₁[f * t,s1,s3]
let f be Function; :: thesis: ( f is_e.translation_of Free (S,Y),s2,s3 implies S₁[f * t,s1,s3] )
assume f is_e.translation_of Free (S,Y),s2,s3 ; :: thesis: S₁[f * t,s1,s3]
then consider o being OperSymbol of S such that
B1: ( the_result_sort_of o = s3 & ex i being Element of NAT st
( i in dom (the_arity_of o) & (the_arity_of o) /. i = s2 & ex a being Function st
( a in Args (o,(Free (S,Y))) & f = transl (o,i,a,(Free (S,Y))) ) ) ) by MSUALG_6:def 5;
consider i being Element of NAT such that
B2: ( i in dom (the_arity_of o) & (the_arity_of o) /. i = s2 & ex a being Function st
( a in Args (o,(Free (S,Y))) & f = transl (o,i,a,(Free (S,Y))) ) ) by B1;
consider a being Function such that
B3: ( a in Args (o,(Free (S,Y))) & f = transl (o,i,a,(Free (S,Y))) ) by B2;
reconsider a = a as Element of Args (o,(Free (S,Y))) by B3;
let V be finite set ; :: thesis: ex x being Element of Y . s1 ex C being context of x st
( x nin V & the_sort_of C = s3 & f * t = transl C )
( [s2,s3] in TranslationRel S & i in dom a ) by B1, B2, MSUALG_6:2, MSUALG_6:def 3;
then consider y being Element of Y . s2, C being context of y, q1 being Element of Args (o,(Free (S,Y))) such that
B4: ( y nin V & q1 = a +* (i,(y -term)) & q1 is y -context_including & y -context_in q1 = y -term & C = o -term q1 & i = y -context_pos_in q1 & transl C = transl (o,i,a,(Free (S,Y))) ) by B2, Th91;
consider y1 being Element of Y . s1, C1 being context of y1 such that
B5: ( y1 nin V \/ (vf C) & the_sort_of C1 = s2 & t = transl C1 ) by Z1;
y in vf C by Th95;
then ( y1 nin vf C & y <> y1 ) by B5, XBOOLE_0:def 3;
then ( C is y1 -omitting & y is y1 -different ) by Th92;
then reconsider C2 = C -sub C1 as context of y1 by B5, Th94;
take y1 ; :: thesis: ex C being context of y1 st
( y1 nin V & the_sort_of C = s3 & f * t = transl C )
take C2 ; :: thesis: ( y1 nin V & the_sort_of C2 = s3 & f * t = transl C2 )
thus y1 nin V by B5, XBOOLE_0:def 3; :: thesis: ( the_sort_of C2 = s3 & f * t = transl C2 )
the_sort_of C2 = the_sort_of C by SORT;
hence the_sort_of C2 = s3 by B1, B4, Th8; :: thesis: f * t = transl C2
thus f * t = transl C2 by B3, B4, B5, Th93; :: thesis: verum

end;

for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds
for t being Translation of Free (S,Y),s1,s2 holds S₁[t,s1,s2] from MSUALG_6:sch 1(A1, A2);
then ex x being Element of Y . s1 ex C being context of x st
( x nin {} & the_sort_of C = s2 & g1 = transl C ) by REACH;
hence ex y11 being Element of Y . s1 ex C12 being context of y11 st
( the_sort_of C12 = s2 & g1 = transl C12 ) ; :: thesis: verum