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 that
A9: for a being Element of Z_2
for c being Subset of X holds f . a,c = a \*\ c and
A10: for a being Element of Z_2
for c being Subset of X holds g . a,c = a \*\ c ; :: thesis: f = g
dom f = [:the carrier of Z_2 ,(bool X):] by FUNCT_2:def 1;
then A11: dom f = dom g by FUNCT_2:def 1;
for x being set st x in dom f holds
f . x = g . x

proof

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

end;

hence f = g by A11, FUNCT_1:9; :: thesis: verum