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:88, TARSKI:def 2;

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

then A2: a * b = 0. Z_2 by VECTSP_1:39;
a \*\ (b \*\ c) = {} X by A1, Def4;
hence a \*\ (b \*\ c) = (a * b) \*\ c by A2, Def4; :: thesis: verum

end;

suppose A3: 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 A3, VECTSP_1:def 16; :: thesis: verum

end;

end;