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 * (b * x)

let a, b be Element of Z_2; :: thesis: for x being Element of (bspace X) holds (a * b) * x = a * (b * x)

let x be Element of (bspace X); :: thesis: (a * b) * x = a * (b * x)

reconsider c = x as Subset of X ;

(a * b) * x = (a * b) \*\ c by Lm2

.= a \*\ (b \*\ c) by Th20

.= a * (b * x) by Lm2 ;

hence (a * b) * x = a * (b * x) ; :: thesis: verum

for x being Element of (bspace X) holds (a * b) * x = a * (b * x)

let a, b be Element of Z_2; :: thesis: for x being Element of (bspace X) holds (a * b) * x = a * (b * x)

let x be Element of (bspace X); :: thesis: (a * b) * x = a * (b * x)

reconsider c = x as Subset of X ;

(a * b) * x = (a * b) \*\ c by Lm2

.= a \*\ (b \*\ c) by Th20

.= a * (b * x) by Lm2 ;

hence (a * b) * x = a * (b * x) ; :: thesis: verum