defpred S_{1}[ set , set , set ] means ex a being Element of Z_2 ex c being Subset of X st

( $1 = a & $2 = c & $3 = a \*\ c );

A1: for x, y being set st x in the carrier of Z_2 & y in bool X holds

ex z being set st

( z in bool X & S_{1}[x,y,z] )

A4: for x, y being set st x in the carrier of Z_2 & y in bool X holds

S_{1}[x,y,f . (x,y)]
from BINOP_1:sch 9(A1);

take f ; :: thesis: for a being Element of Z_2

for c being Subset of X holds f . (a,c) = a \*\ c

for a being Element of Z_2

for c being Subset of X holds f . (a,c) = a \*\ c

for c being Subset of X holds f . (a,c) = a \*\ c ; :: thesis: verum

( $1 = a & $2 = c & $3 = a \*\ c );

A1: for x, y being set st x in the carrier of Z_2 & y in bool X holds

ex z being set st

( z in bool X & S

proof

consider f being Function of [: the carrier of Z_2,(bool X):],(bool X) such that
let x, y be set ; :: thesis: ( x in the carrier of Z_2 & y in bool X implies ex z being set st

( z in bool X & S_{1}[x,y,z] ) )

assume that

A2: x in the carrier of Z_2 and

A3: y in bool X ; :: thesis: ex z being set st

( z in bool X & S_{1}[x,y,z] )

reconsider y = y as Subset of X by A3;

reconsider x = x as Element of Z_2 by A2;

set z = x \*\ y;

take x \*\ y ; :: thesis: ( x \*\ y in bool X & S_{1}[x,y,x \*\ y] )

thus ( x \*\ y in bool X & S_{1}[x,y,x \*\ y] )
; :: thesis: verum

end;( z in bool X & S

assume that

A2: x in the carrier of Z_2 and

A3: y in bool X ; :: thesis: ex z being set st

( z in bool X & S

reconsider y = y as Subset of X by A3;

reconsider x = x as Element of Z_2 by A2;

set z = x \*\ y;

take x \*\ y ; :: thesis: ( x \*\ y in bool X & S

thus ( x \*\ y in bool X & S

A4: for x, y being set st x in the carrier of Z_2 & y in bool X holds

S

take f ; :: thesis: for a being Element of Z_2

for c being Subset of X holds f . (a,c) = a \*\ c

for a being Element of Z_2

for c being Subset of X holds f . (a,c) = a \*\ c

proof

hence
for a being Element of Z_2
let a be Element of Z_2; :: thesis: for c being Subset of X holds f . (a,c) = a \*\ c

let c be Subset of X; :: thesis: f . (a,c) = a \*\ c

ex a9 being Element of Z_2 ex c9 being Subset of X st

( a = a9 & c = c9 & f . (a,c) = a9 \*\ c9 ) by A4;

hence f . (a,c) = a \*\ c ; :: thesis: verum

end;let c be Subset of X; :: thesis: f . (a,c) = a \*\ c

ex a9 being Element of Z_2 ex c9 being Subset of X st

( a = a9 & c = c9 & f . (a,c) = a9 \*\ c9 ) by A4;

hence f . (a,c) = a \*\ c ; :: thesis: verum

for c being Subset of X holds f . (a,c) = a \*\ c ; :: thesis: verum