defpred S1[ 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 S1[x,y]
proof
let x be object ; :: thesis: ( x in the carrier' of S implies ex y being object st S1[x,y] )
assume x in the carrier' of S ; :: thesis: ex y being object st S1[x,y]
then reconsider o = x as OperSymbol of S ;
take DenOp (o,X) ; :: thesis: S1[x, DenOp (o,X)]
thus S1[x, DenOp (o,X)] ; :: thesis: verum
end;
consider f being Function such that
A2: ( dom f = the carrier' of S & ( for x being object st x in the carrier' of S holds
S1[x,f . x] ) ) from reconsider f = f as ManySortedSet of the carrier' of S by ;
for x being object st x in dom f holds
f . x is Function
proof
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;
then reconsider f = f as ManySortedFunction of the carrier' of S by FUNCOP_1:def 6;
for x being object st x in the carrier' of S holds
f . x is Function of (((() #) * the Arity of S) . x),((() * the ResultSort of S) . x)
proof
let x be object ; :: thesis: ( x in the carrier' of S implies f . x is Function of (((() #) * the Arity of S) . x),((() * the ResultSort of S) . x) )
assume x in the carrier' of S ; :: thesis: f . x is Function of (((() #) * the Arity of S) . 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 (((() #) * the Arity of S) . x),((() * the ResultSort of S) . x) ; :: thesis: verum
end;
then reconsider f = f as ManySortedFunction of (() #) * the Arity of S,() * the ResultSort of S by PBOOLE:def 15;
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