thus dL-Z_2 is add-associative :: thesis: dL-Z_2 is distributive

proof

thus for a, b, c being Element of dL-Z_2 holds (a + b) + c = a + (b + c) by Lm20; :: according to RLVECT_1:def 6 :: thesis: verum

end;

thus dL-Z_2 is distributive :: thesis: verum

proof

let a, b, d be Element of dL-Z_2 ; :: according to VECTSP_1:def 18 :: 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 Lm2, CARD_1:88, TARSKI:def 2;
hence a * (b + d) = (a * b) + (a * d) by Lm6, Lm7, Lm8, Lm9, Lm13, Lm14, Lm15, Lm16; :: thesis: (b + d) * a = (b * a) + (d * a)
thus (b + d) * a = (b * a) + (d * a) by A1, Lm6, Lm7, Lm8, Lm9, Lm13, Lm14, Lm15, Lm16; :: thesis: verum

end;