defpred S1[ object , object ] means for o being OperSymbol of S st o = $1 holds
$2 = OSQuotArgs (R,o);
set O = the carrier' of S;
A5:
for x being object st x in the carrier' of S holds
ex y being object st S1[x,y]
consider f being Function such that
A6:
( dom f = the carrier' of S & ( for x being object st x in the carrier' of S holds
S1[x,f . x] ) )
from CLASSES1:sch 1(A5);
reconsider f = f as ManySortedSet of the carrier' of S by A6, PARTFUN1:def 2, RELAT_1:def 18;
for x being object st x in dom f holds
f . x is Function
then reconsider f = f as ManySortedFunction of the carrier' of S by FUNCOP_1:def 6;
for i being object st i in the carrier' of S holds
f . i is Function of ((( the Sorts of A #) * the Arity of S) . i),((((OSClass R) #) * the Arity of S) . i)
then reconsider f = f as ManySortedFunction of ( the Sorts of A #) * the Arity of S,((OSClass R) #) * the Arity of S by PBOOLE:def 15;
take
f
; for o being OperSymbol of S holds f . o = OSQuotArgs (R,o)
thus
for o being OperSymbol of S holds f . o = OSQuotArgs (R,o)
by A6; verum