let f, g be Function of [: the carrier of Z_2,(bool X):],(bool X); :: 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 g . (a,c) = a \*\ c ) implies f = g )
assume A5: ( ( 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 g . (a,c) = a \*\ c ) ) ; :: thesis: f = g
A6: for x being object st x in dom f holds
f . x = g . x

proof

let x be object ; :: thesis: ( x in dom f implies f . x = g . x )
assume x in dom f ; :: thesis: f . x = g . x
then consider y, z being object such that
A7: y in the carrier of Z_2 and
A8: z in bool X and
A9: x = [y,z] by ZFMISC_1:def 2;
reconsider z = z as Subset of X by A8;
reconsider y = y as Element of Z_2 by A7;
( f . (y,z) = y \*\ z & g . (y,z) = y \*\ z ) by A5;
hence f . x = g . x by A9; :: thesis: verum

end;

dom f = [: the carrier of Z_2,(bool X):] by FUNCT_2:def 1;
then dom f = dom g by FUNCT_2:def 1;
hence f = g by A6; :: thesis: verum