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

per cases ( a = 0. Z_2 or a = 1. Z_2 ) by Th5, Th6, CARD_1:50, TARSKI:def 2;

suppose A1: a = 0. Z_2 ; :: thesis: a \*\ (b \*\ c) = (a * b) \*\ c

then a \*\ (b \*\ c) = {} X by Def4;
hence a \*\ (b \*\ c) = (a * b) \*\ c by A1, Def4; :: thesis: verum

end;

suppose A2: a = 1. Z_2 ; :: thesis: a \*\ (b \*\ c) = (a * b) \*\ c

then a \*\ (b \*\ c) = b \*\ c by Def4;
hence a \*\ (b \*\ c) = (a * b) \*\ c by A2; :: thesis: verum

end;

end;