defpred S1[ set , set ] 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 set st S1[x,y] & S1[x,z] holds
y = z
proof
let x,
y,
z be
set ;
:: 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 &
x = [the carrier of S1,the carrier' of S1,the Arity of S1,the ResultSort of S1] &
S2 = z &
x = [the carrier of S2,the carrier' of S2,the Arity of S2,the ResultSort of S2] & (
S2 is
empty implies
S2 is
void ) )
;
( the
carrier of
S1 = the
carrier of
S2 & the
carrier' of
S1 = the
carrier' of
S2 & the
Arity of
S1 = the
Arity of
S2 & the
ResultSort of
S1 = the
ResultSort of
S2 )
by A2, MCART_1:33;
hence
y = z
by A2;
:: thesis: verum
end;
consider X being set such that
A3:
for x being set holds
( x in X iff ex y being set st
( y in [:(bool A),(bool A),(PFuncs A,(A * )),(PFuncs A,A):] & S1[y,x] ) )
from TARSKI:sch 1(A1);
take
X
; :: thesis: for x being set 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 set ; :: 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: verumproof
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
set such that A4:
(
y in [:(bool A),(bool A),(PFuncs A,(A * )),(PFuncs A,A):] &
S1[
y,
x] )
by A3;
consider S being non
empty non
void strict ManySortedSign such that A5:
(
S = x &
y = [the carrier of S,the carrier' of S,the Arity of S,the ResultSort of S] )
by A4;
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 A4, A5, MCART_1:84;
hence
(
x = S & the
carrier of
S c= A & the
carrier' of
S c= A )
by A5;
:: thesis: verum
end;
given S being non
empty non
void strict ManySortedSign such that A6:
(
x = S & the
carrier of
S c= A & the
carrier' of
S c= A )
;
:: thesis: x in X
consider y being
set such that A7:
y = [the carrier of S,the carrier' of S,the Arity of S,the ResultSort of S]
;
reconsider C = the
carrier of
S as
Subset of
A by A6;
A8:
C * c= A *
by MSUHOM_1:2;
A9:
(
dom the
Arity of
S c= A &
rng the
Arity of
S c= the
carrier of
S * )
by A6, FUNCT_2:def 1;
rng the
Arity of
S c= A *
by A8, XBOOLE_1:1;
then A10:
the
Arity of
S in PFuncs A,
(A * )
by A9, PARTFUN1:def 5;
A11:
dom the
ResultSort of
S = the
carrier' of
S
by FUNCT_2:def 1;
rng the
ResultSort of
S c= A
by A6, XBOOLE_1:1;
then
the
ResultSort of
S in PFuncs A,
A
by A6, A11, PARTFUN1:def 5;
then
y in [:(bool A),(bool A),(PFuncs A,(A * )),(PFuncs A,A):]
by A6, A7, A10, MCART_1:84;
hence
x in X
by A3, A6, A7;
:: thesis: verum
end;