defpred S₁[ Element of (Free (S,X))] means the_sort_of S is s -reachable ;
s is s -reachable by REWRITE1:12;
then A1: S₁[x -term ] by SORT;
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
A3: p is x -context_including and
A4: S₁[x -context_in p] ; :: thesis: for C being context of x st C = o -term p holds
S₁[C]
let C be context of x; :: thesis: ( C = o -term p implies S₁[C] )
assume AA: C = o -term p ; :: thesis: S₁[C]
A6: the_sort_of C = the_result_sort_of o by AA, Th8;
A5: ( x -context_pos_in p in dom p & dom p = dom (the_arity_of o) & x -context_in p = p . (x -context_pos_in p) ) by A3, Th71, MSUALG_6:2;
( x -context_in p in the Sorts of (Free (S,X)) . ((the_arity_of o) /. (x -context_pos_in p)) & the Sorts of (Free (S,X)) . ((the_arity_of o) /. (x -context_pos_in p)) = the Sorts of (Free (S,X)) . ((the_arity_of o) . (x -context_pos_in p)) ) by A5, MSUALG_6:2, PARTFUN1:def 6;
then ( the_sort_of (x -context_in p) = (the_arity_of o) /. (x -context_pos_in p) & (the_arity_of o) /. (x -context_pos_in p) = (the_arity_of o) . (x -context_pos_in p) & (the_arity_of o) . (x -context_pos_in p) in rng (the_arity_of o) & x -context_pos_in p in NAT ) by A5, SORT, FUNCT_1:def 3, PARTFUN1:def 6;
then [(the_sort_of (x -context_in p)),(the_result_sort_of o)] in TranslationRel S by A5, MSUALG_6:def 3;
then ( TranslationRel S reduces the_sort_of (x -context_in p), the_result_sort_of o & TranslationRel S reduces s, the_sort_of (x -context_in p) ) by A4, REACH, REWRITE1:15;
hence TranslationRel S reduces s, the_sort_of C by A6, REWRITE1:16; :: according to MSAFREE5:def 33 :: thesis: verum

end;

S₁[C] from MSAFREE5:sch 4(A1, A2);
hence the_sort_of C is s -reachable ; :: thesis: verum