let X be set ; :: thesis: for a being Element of Z_2

for c, d being Subset of X holds a \*\ (c \+\ d) = (a \*\ c) \+\ (a \*\ d)

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

let c, d be Subset of X; :: thesis: a \*\ (c \+\ d) = (a \*\ c) \+\ (a \*\ d)

for c, d being Subset of X holds a \*\ (c \+\ d) = (a \*\ c) \+\ (a \*\ d)

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

let c, d be Subset of X; :: thesis: a \*\ (c \+\ d) = (a \*\ c) \+\ (a \*\ d)