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 ;
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 ; :: 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 ;
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 ; :: 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 ;
hence (a + b) \*\ c = (a \*\ c) \+\ (b \*\ c) by A2, A4, A5, Def4, Th7; :: thesis: verum
end;
end;
end;
end;