let X be set ; :: thesis: for a, b being Element of Z_2
for c being Subset of X holds (a + b) \*\ c = (a \*\ c) \+\ (b \*\ c)
let a, b be Element of Z_2; :: thesis: for c being Subset of X holds (a + b) \*\ c = (a \*\ c) \+\ (b \*\ c)
let c be Subset of X; :: thesis: (a + b) \*\ c = (a \*\ c) \+\ (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 \*\ c) \+\ (b \*\ c)

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

end;

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

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

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

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

end;

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

A5: c \+\ c = {} X by XBOOLE_1:92;
b \*\ c = c by A4, Def4;
hence (a + b) \*\ c = (a \*\ c) \+\ (b \*\ c) by A2, A4, A5, Def4, Th7; :: thesis: verum

end;

end;

end;

end;