defpred S1[ 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 S1[i,u]
proof
let i be object ; :: thesis: ( i in the carrier of S implies ex u being object st S1[i,u] )
assume i in the carrier of S ; :: thesis: ex u being object st S1[i,u]
then reconsider s = i as SortSymbol of S ;
take Reverse (s,X) ; :: thesis: S1[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;
consider H being Function such that
A2: ( dom H = the carrier of S & ( for i being object st i in the carrier of S holds
S1[i,H . i] ) ) from reconsider H = H as ManySortedSet of the carrier of S by ;
for x being object st x in dom H holds
H . x is Function
proof
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;
then reconsider H = H as ManySortedFunction of the carrier of S by FUNCOP_1:def 6;
for i being object st i in the carrier of S holds
H . i is Function of (() . i),(X . i)
proof
let i be object ; :: thesis: ( i in the carrier of S implies H . i is Function of (() . i),(X . i) )
assume i in the carrier of S ; :: thesis: H . i is Function of (() . i),(X . i)
then reconsider s = i as SortSymbol of S ;
( (FreeGen X) . s = FreeGen (s,X) & H . i = Reverse (s,X) ) by ;
hence H . i is Function of (() . i),(X . i) ; :: thesis: verum
end;
then reconsider H = H as ManySortedFunction of FreeGen X,X by PBOOLE:def 15;
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