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