for a, b, c being Element of dL-Z_2 holds (a + b) + c = a + (b + c) by Lm22;
hence dL-Z_2 is add-associative ; :: thesis: dL-Z_2 is distributive
thus dL-Z_2 is distributive :: thesis: verum
proof
let a, b, d be Element of dL-Z_2; :: according to VECTSP_1:def 7 :: thesis: ( a * (b + d) = (a * b) + (a * d) & (b + d) * a = (b * a) + (d * a) )
A1: ( ( a = In (0,2) & b = In (0,2) & d = In (0,2) ) or ( a = In (0,2) & b = In (0,2) & d = In (1,2) ) or ( a = In (0,2) & b = In (1,2) & d = In (0,2) ) or ( a = In (0,2) & b = In (1,2) & d = In (1,2) ) or ( a = In (1,2) & b = In (0,2) & d = In (0,2) ) or ( a = In (1,2) & b = In (0,2) & d = In (1,2) ) or ( a = In (1,2) & b = In (1,2) & d = In (0,2) ) or ( a = In (1,2) & b = In (1,2) & d = In (1,2) ) ) by Lm3, Lm4, CARD_1:50, TARSKI:def 2;
hence a * (b + d) = (a * b) + (a * d) by Lm8, Lm9, Lm10, Lm11, Lm15, Lm16, Lm17, Lm18; :: thesis: (b + d) * a = (b * a) + (d * a)
thus (b + d) * a = (b * a) + (d * a) by A1, Lm8, Lm9, Lm10, Lm11, Lm15, Lm16, Lm17, Lm18; :: thesis: verum
end;