set I = the carrier of S;
set FG = OSFreeGen X;
defpred S₁[ set , set ] means for s being Element of S st s = $1 holds
$2 = NHReverse s,X;
A1: for i being set st i in the carrier of S holds
ex u being set st S₁[i,u]

proof

let i be set ; :: thesis: ( i in the carrier of S implies ex u being set st S₁[i,u] )
assume i in the carrier of S ; :: thesis: ex u being set st S₁[i,u]
then reconsider s = i as SortSymbol of S ;
take NHReverse s,X ; :: thesis: S₁[i, NHReverse s,X]
let s1 be Element of S; :: thesis: ( s1 = i implies NHReverse s,X = NHReverse s1,X )
assume s1 = i ; :: thesis: NHReverse s,X = NHReverse s1,X
hence NHReverse s,X = NHReverse s1,X ; :: thesis: verum

end;

consider H being Function such that
A2: ( dom H = the carrier of S & ( for i being set st i in the carrier of S holds
S₁[i,H . i] ) ) from CLASSES1:sch 1(A1);
reconsider H = H as ManySortedSet of by A2, PARTFUN1:def 4, RELAT_1:def 18;
for x being set st x in dom H holds
H . x is Function

proof

let i be set ; :: thesis: ( i in dom H implies H . i is Function )
assume i in dom H ; :: thesis: H . i is Function
then reconsider s = i as SortSymbol of S by A2;
H . s = NHReverse s,X by A2;
hence H . i is Function ; :: thesis: verum

end;

then reconsider H = H as ManySortedFunction of by FUNCOP_1:def 6;
for i being set st i in the carrier of S holds
H . i is Function of ((OSFreeGen X) . i),((PTVars X) . i)

proof

let i be set ; :: thesis: ( i in the carrier of S implies H . i is Function of ((OSFreeGen X) . i),((PTVars X) . i) )
assume i in the carrier of S ; :: thesis: H . i is Function of ((OSFreeGen X) . i),((PTVars X) . i)
then reconsider s = i as SortSymbol of S ;
A3: ( (OSFreeGen X) . s = OSFreeGen s,X & (PTVars X) . s = PTVars s,X ) by Def25, Def27;
H . i = NHReverse s,X by A2;
hence H . i is Function of ((OSFreeGen X) . i),((PTVars X) . i) by A3; :: thesis: verum

end;

then reconsider H = H as ManySortedFunction of OSFreeGen X, PTVars X by PBOOLE:def 18;
take H ; :: thesis: for s being Element of S holds H . s = NHReverse s,X
let s be Element of S; :: thesis: H . s = NHReverse s,X
thus H . s = NHReverse s,X by A2; :: thesis: verum