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

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