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

$2 = DenOp (o,X);

set Y = the carrier' of S;

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 ((((FreeSort X) #) * the Arity of S) . x),(((FreeSort X) * the ResultSort of S) . x)

take f ; :: thesis: for o being OperSymbol of S holds f . o = DenOp (o,X)

let o be OperSymbol of S; :: thesis: f . o = DenOp (o,X)

thus f . o = DenOp (o,X) by A2; :: thesis: verum

$2 = DenOp (o,X);

set Y = the carrier' of S;

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 DenOp (o,X) ; :: thesis: S_{1}[x, DenOp (o,X)]

thus S_{1}[x, DenOp (o,X)]
; :: 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 DenOp (o,X) ; :: 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 ;

f . o = DenOp (o,X) 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 ;

f . o = DenOp (o,X) 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 ((((FreeSort X) #) * the Arity of S) . x),(((FreeSort X) * the ResultSort of S) . x)

proof

then reconsider f = f as ManySortedFunction of ((FreeSort X) #) * the Arity of S,(FreeSort X) * 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 ((((FreeSort X) #) * the Arity of S) . x),(((FreeSort X) * the ResultSort of S) . x) )

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

then reconsider o = x as OperSymbol of S ;

f . o = DenOp (o,X) by A2;

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

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

then reconsider o = x as OperSymbol of S ;

f . o = DenOp (o,X) by A2;

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

take f ; :: thesis: for o being OperSymbol of S holds f . o = DenOp (o,X)

let o be OperSymbol of S; :: thesis: f . o = DenOp (o,X)

thus f . o = DenOp (o,X) by A2; :: thesis: verum