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)

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;

end;

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;hence (a + b) \*\ c = (a \*\ c) \+\ (b \*\ c) by A1, RLVECT_1:4; :: thesis: verum

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

end;