set O = the carrier' of S;
defpred S₁[ set , set ] means for o being OperSymbol of S st o = $1 holds
$2 = QuotArgs R,o;
A7: for x being set st x in the carrier' of S holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in the carrier' of S implies ex y being set st S₁[x,y] )
assume x in the carrier' of S ; :: thesis: ex y being set st S₁[x,y]
then reconsider x1 = x as OperSymbol of S ;
take QuotArgs R,x1 ; :: thesis: S₁[x, QuotArgs R,x1]
thus S₁[x, QuotArgs R,x1] ; :: thesis: verum

end;

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

proof

let x be set ; :: thesis: ( x in dom f implies f . x is Function )
assume x in dom f ; :: thesis: f . x is Function
then reconsider x1 = x as OperSymbol of S by A8;
f . x1 = QuotArgs R,x1 by A8;
hence f . x is Function ; :: thesis: verum

end;

then reconsider f = f as ManySortedFunction of by FUNCOP_1:def 6;
for i being set st i in the carrier' of S holds
f . i is Function of (((the Sorts of A # ) * the Arity of S) . i),((((Class R) # ) * the Arity of S) . i)

proof

let i be set ; :: thesis: ( i in the carrier' of S implies f . i is Function of (((the Sorts of A # ) * the Arity of S) . i),((((Class R) # ) * the Arity of S) . i) )
assume i in the carrier' of S ; :: thesis: f . i is Function of (((the Sorts of A # ) * the Arity of S) . i),((((Class R) # ) * the Arity of S) . i)
then reconsider i1 = i as OperSymbol of S ;
f . i1 = QuotArgs R,i1 by A8;
hence f . i is Function of (((the Sorts of A # ) * the Arity of S) . i),((((Class R) # ) * the Arity of S) . i) ; :: thesis: verum

end;

then reconsider f = f as ManySortedFunction of (the Sorts of A # ) * the Arity of S,((Class R) # ) * the Arity of S by PBOOLE:def 18;
take f ; :: thesis: for o being OperSymbol of S holds f . o = QuotArgs R,o
for x being OperSymbol of S holds f . x = QuotArgs R,x by A8;
hence for o being OperSymbol of S holds f . o = QuotArgs R,o ; :: thesis: verum