defpred S_{1}[ object , object ] means for s being SortSymbol of S st s = $1 holds

$2 = Reverse (s,X);

set I = the carrier of S;

set FG = FreeGen X;

A1: for i being object st i in the carrier of S holds

ex u being object st S_{1}[i,u]

A2: ( dom H = the carrier of S & ( for i being object st i in the carrier of S holds

S_{1}[i,H . i] ) )
from CLASSES1:sch 1(A1);

reconsider H = H as ManySortedSet of the carrier of S by A2, PARTFUN1:def 2, RELAT_1:def 18;

for x being object st x in dom H holds

H . x is Function

for i being object st i in the carrier of S holds

H . i is Function of ((FreeGen X) . i),(X . i)

take H ; :: thesis: for s being SortSymbol of S holds H . s = Reverse (s,X)

let s be SortSymbol of S; :: thesis: H . s = Reverse (s,X)

thus H . s = Reverse (s,X) by A2; :: thesis: verum

$2 = Reverse (s,X);

set I = the carrier of S;

set FG = FreeGen X;

A1: for i being object st i in the carrier of S holds

ex u being object st S

proof

consider H being Function such that
let i be object ; :: thesis: ( i in the carrier of S implies ex u being object st S_{1}[i,u] )

assume i in the carrier of S ; :: thesis: ex u being object st S_{1}[i,u]

then reconsider s = i as SortSymbol of S ;

take Reverse (s,X) ; :: thesis: S_{1}[i, Reverse (s,X)]

let s1 be SortSymbol of S; :: thesis: ( s1 = i implies Reverse (s,X) = Reverse (s1,X) )

assume s1 = i ; :: thesis: Reverse (s,X) = Reverse (s1,X)

hence Reverse (s,X) = Reverse (s1,X) ; :: thesis: verum

end;assume i in the carrier of S ; :: thesis: ex u being object st S

then reconsider s = i as SortSymbol of S ;

take Reverse (s,X) ; :: thesis: S

let s1 be SortSymbol of S; :: thesis: ( s1 = i implies Reverse (s,X) = Reverse (s1,X) )

assume s1 = i ; :: thesis: Reverse (s,X) = Reverse (s1,X)

hence Reverse (s,X) = Reverse (s1,X) ; :: thesis: verum

A2: ( dom H = the carrier of S & ( for i being object st i in the carrier of S holds

S

reconsider H = H as ManySortedSet of the carrier of S by A2, PARTFUN1:def 2, RELAT_1:def 18;

for x being object st x in dom H holds

H . x is Function

proof

then reconsider H = H as ManySortedFunction of the carrier of S by FUNCOP_1:def 6;
let i be object ; :: 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 ;

H . s = Reverse (s,X) by A2;

hence H . i is Function ; :: thesis: verum

end;assume i in dom H ; :: thesis: H . i is Function

then reconsider s = i as SortSymbol of S ;

H . s = Reverse (s,X) by A2;

hence H . i is Function ; :: thesis: verum

for i being object st i in the carrier of S holds

H . i is Function of ((FreeGen X) . i),(X . i)

proof

then reconsider H = H as ManySortedFunction of FreeGen X,X by PBOOLE:def 15;
let i be object ; :: thesis: ( i in the carrier of S implies H . i is Function of ((FreeGen X) . i),(X . i) )

assume i in the carrier of S ; :: thesis: H . i is Function of ((FreeGen X) . i),(X . i)

then reconsider s = i as SortSymbol of S ;

( (FreeGen X) . s = FreeGen (s,X) & H . i = Reverse (s,X) ) by A2, Def16;

hence H . i is Function of ((FreeGen X) . i),(X . i) ; :: thesis: verum

end;assume i in the carrier of S ; :: thesis: H . i is Function of ((FreeGen X) . i),(X . i)

then reconsider s = i as SortSymbol of S ;

( (FreeGen X) . s = FreeGen (s,X) & H . i = Reverse (s,X) ) by A2, Def16;

hence H . i is Function of ((FreeGen X) . i),(X . i) ; :: thesis: verum

take H ; :: thesis: for s being SortSymbol of S holds H . s = Reverse (s,X)

let s be SortSymbol of S; :: thesis: H . s = Reverse (s,X)

thus H . s = Reverse (s,X) by A2; :: thesis: verum