defpred S1[ 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 & S1[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 & S1[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 & S1[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 & S1[x,y,x \*\ y] )
thus ( x \*\ y in bool X & S1[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
S1[x,y,f . (x,y)] from 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