set B = (A #) * the Arity of S;

set C = A * the ResultSort of S;

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

$2 = o /. A;

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

ex y being object st S_{1}[x,y]

A2: ( dom f = the carrier' of S & ( for x being object st x in the carrier' of S holds

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

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

for x being object st x in dom f holds

f . x is Function

for x being object st x in the carrier' of S holds

f . x is Function of (((A #) * the Arity of S) . x),((A * the ResultSort of S) . x)

take f ; :: thesis: for o being OperSymbol of S holds f . o = o /. A

let o be OperSymbol of S; :: thesis: f . o = o /. A

thus f . o = o /. A by A2; :: thesis: verum

set C = A * the ResultSort of S;

defpred S

$2 = o /. A;

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

ex y being object st S

proof

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

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

then reconsider o = x as OperSymbol of S ;

take o /. A ; :: thesis: S_{1}[x,o /. A]

thus S_{1}[x,o /. A]
; :: thesis: verum

end;assume x in the carrier' of S ; :: thesis: ex y being object st S

then reconsider o = x as OperSymbol of S ;

take o /. A ; :: thesis: S

thus S

A2: ( dom f = the carrier' of S & ( for x being object st x in the carrier' of S holds

S

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

for x being object st x in dom f holds

f . x is Function

proof

then reconsider f = f as ManySortedFunction of the carrier' of S by FUNCOP_1:def 6;
let x be object ; :: thesis: ( x in dom f implies f . x is Function )

assume x in dom f ; :: thesis: f . x is Function

then reconsider o = x as OperSymbol of S by A2;

f . o = o /. A by A2;

hence f . x is Function ; :: thesis: verum

end;assume x in dom f ; :: thesis: f . x is Function

then reconsider o = x as OperSymbol of S by A2;

f . o = o /. A by A2;

hence f . x is Function ; :: thesis: verum

for x being object st x in the carrier' of S holds

f . x is Function of (((A #) * the Arity of S) . x),((A * the ResultSort of S) . x)

proof

then reconsider f = f as ManySortedFunction of (A #) * the Arity of S,A * the ResultSort of S by PBOOLE:def 15;
let x be object ; :: thesis: ( x in the carrier' of S implies f . x is Function of (((A #) * the Arity of S) . x),((A * the ResultSort of S) . x) )

assume x in the carrier' of S ; :: thesis: f . x is Function of (((A #) * the Arity of S) . x),((A * the ResultSort of S) . x)

then reconsider o = x as OperSymbol of S ;

f . o = o /. A by A2;

hence f . x is Function of (((A #) * the Arity of S) . x),((A * the ResultSort of S) . x) ; :: thesis: verum

end;assume x in the carrier' of S ; :: thesis: f . x is Function of (((A #) * the Arity of S) . x),((A * the ResultSort of S) . x)

then reconsider o = x as OperSymbol of S ;

f . o = o /. A by A2;

hence f . x is Function of (((A #) * the Arity of S) . x),((A * the ResultSort of S) . x) ; :: thesis: verum

take f ; :: thesis: for o being OperSymbol of S holds f . o = o /. A

let o be OperSymbol of S; :: thesis: f . o = o /. A

thus f . o = o /. A by A2; :: thesis: verum