defpred S1[ object , object ] means ex S being non empty non void strict ManySortedSign st
( S = \$2 & \$1 = [ the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S] );
A1: for x, y, z being object st S1[x,y] & S1[x,z] holds
y = z
proof
let x, y, z be object ; :: thesis: ( S1[x,y] & S1[x,z] implies y = z )
assume ( S1[x,y] & S1[x,z] ) ; :: thesis: y = z
then consider S1, S2 being non empty non void strict ManySortedSign such that
A2: S1 = y and
A3: x = [ the carrier of S1, the carrier' of S1, the Arity of S1, the ResultSort of S1] and
A4: S2 = z and
A5: x = [ the carrier of S2, the carrier' of S2, the Arity of S2, the ResultSort of S2] and
( S2 is empty implies S2 is void ) ;
A6: the Arity of S1 = the Arity of S2 by ;
( the carrier of S1 = the carrier of S2 & the carrier' of S1 = the carrier' of S2 ) by ;
hence y = z by A2, A3, A4, A5, A6, XTUPLE_0:5; :: thesis: verum
end;
consider X being set such that
A7: for x being object holds
( x in X iff ex y being object st
( y in [:(bool A),(bool A),(PFuncs (A,(A *))),(PFuncs (A,A)):] & S1[y,x] ) ) from take X ; :: thesis: for x being object holds
( x in X iff ex S being non empty non void strict ManySortedSign st
( x = S & the carrier of S c= A & the carrier' of S c= A ) )

let x be object ; :: thesis: ( x in X iff ex S being non empty non void strict ManySortedSign st
( x = S & the carrier of S c= A & the carrier' of S c= A ) )

thus ( x in X iff ex S being non empty non void strict ManySortedSign st
( x = S & the carrier of S c= A & the carrier' of S c= A ) ) :: thesis: verum
proof
thus ( x in X implies ex S being non empty non void strict ManySortedSign st
( x = S & the carrier of S c= A & the carrier' of S c= A ) ) :: thesis: ( ex S being non empty non void strict ManySortedSign st
( x = S & the carrier of S c= A & the carrier' of S c= A ) implies x in X )
proof
assume x in X ; :: thesis: ex S being non empty non void strict ManySortedSign st
( x = S & the carrier of S c= A & the carrier' of S c= A )

then consider y being object such that
A8: y in [:(bool A),(bool A),(PFuncs (A,(A *))),(PFuncs (A,A)):] and
A9: S1[y,x] by A7;
consider S being non empty non void strict ManySortedSign such that
A10: S = x and
y = [ the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S] by A9;
take S ; :: thesis: ( x = S & the carrier of S c= A & the carrier' of S c= A )
( the carrier of S in bool A & the carrier' of S in bool A ) by ;
hence ( x = S & the carrier of S c= A & the carrier' of S c= A ) by A10; :: thesis: verum
end;
given S being non empty non void strict ManySortedSign such that A11: x = S and
A12: the carrier of S c= A and
A13: the carrier' of S c= A ; :: thesis: x in X
( dom the ResultSort of S = the carrier' of S & rng the ResultSort of S c= A ) by ;
then A14: the ResultSort of S in PFuncs (A,A) by ;
reconsider C = the carrier of S as Subset of A by A12;
consider y being set such that
A15: y = [ the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S] ;
C * c= A * by MSUHOM_1:2;
then A16: rng the Arity of S c= A * ;
dom the Arity of S c= A by A13;
then the Arity of S in PFuncs (A,(A *)) by ;
then y in [:(bool A),(bool A),(PFuncs (A,(A *))),(PFuncs (A,A)):] by ;
hence x in X by A7, A11, A15; :: thesis: verum
end;