defpred S₁[ 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₁[x,y,z] )

proof

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₁[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₁[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₁[x,y,x \*\ y] )
thus ( x \*\ y in bool X & S₁[x,y,x \*\ y] ) ; :: thesis: verum

end;

consider f being Function of [: the carrier of Z_2,(bool X):],(bool X) such that
A4: for x, y being set st x in the carrier of Z_2 & y in bool X holds
S₁[x,y,f . (x,y)] from BINOP_1:sch 1(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

proof

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;

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