defpred S_{1}[ 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 S_{1}[x,y] & S_{1}[x,z] holds

y = z

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)):] & S_{1}[y,x] ) )
from TARSKI:sch 1(A1);

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

( 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 S

y = z

proof

consider X being set such that
let x, y, z be object ; :: thesis: ( S_{1}[x,y] & S_{1}[x,z] implies y = z )

assume ( S_{1}[x,y] & S_{1}[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 A3, A5, XTUPLE_0:5;

( the carrier of S1 = the carrier of S2 & the carrier' of S1 = the carrier' of S2 ) by A3, A5, XTUPLE_0:5;

hence y = z by A2, A3, A4, A5, A6, XTUPLE_0:5; :: thesis: verum

end;assume ( S

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 A3, A5, XTUPLE_0:5;

( the carrier of S1 = the carrier of S2 & the carrier' of S1 = the carrier' of S2 ) by A3, A5, XTUPLE_0:5;

hence y = z by A2, A3, A4, A5, A6, XTUPLE_0:5; :: thesis: verum

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)):] & S

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 )

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 A12, FUNCT_2:def 1;

then A14: the ResultSort of S in PFuncs (A,A) by A13, PARTFUN1:def 3;

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 A16, PARTFUN1:def 3;

then y in [:(bool A),(bool A),(PFuncs (A,(A *))),(PFuncs (A,A)):] by A12, A13, A15, A14, MCART_1:80;

hence x in X by A7, A11, A15; :: thesis: verum

end;( 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

given S being non empty non void strict ManySortedSign such that A11:
x = S
and
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: S_{1}[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 A8, A9, A10, MCART_1:80;

hence ( x = S & the carrier of S c= A & the carrier' of S c= A ) by A10; :: thesis: verum

end;( 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: S

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 A8, A9, A10, MCART_1:80;

hence ( x = S & the carrier of S c= A & the carrier' of S c= A ) by A10; :: thesis: verum

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 A12, FUNCT_2:def 1;

then A14: the ResultSort of S in PFuncs (A,A) by A13, PARTFUN1:def 3;

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 A16, PARTFUN1:def 3;

then y in [:(bool A),(bool A),(PFuncs (A,(A *))),(PFuncs (A,A)):] by A12, A13, A15, A14, MCART_1:80;

hence x in X by A7, A11, A15; :: thesis: verum