let X be set ; :: thesis: for a, b being Element of Z_2
for x being Element of (bspace X) holds (a + b) * x = (a * x) + (b * x)
let a, b be Element of Z_2; :: thesis: for x being Element of (bspace X) holds (a + b) * x = (a * x) + (b * x)
let x be Element of (bspace X); :: thesis: (a + b) * x = (a * x) + (b * x)
reconsider c = x as Subset of X ;
(a + b) * x = (a + b) \*\ c by Lm2
.= (a \*\ c) \+\ (b \*\ c) by Th18
.= (a * x) + (b * x) by Lm2 ;
hence (a + b) * x = (a * x) + (b * x) ; :: thesis: verum