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

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