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