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)

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 \*\ (c \+\ d) = (a \*\ c) \+\ (a \*\ d)

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

end;

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

then ( a \*\ (c \+\ d) = c \+\ d & a \*\ c = c ) by Def4;
hence a \*\ (c \+\ d) = (a \*\ c) \+\ (a \*\ d) by A2, Def4; :: thesis: verum

end;

end;