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

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