let X be set ; :: thesis: ( bspace X is vector-distributive & bspace X is scalar-distributive & bspace X is scalar-associative & bspace X is scalar-unital )
thus bspace X is vector-distributive :: thesis: ( bspace X is scalar-distributive & bspace X is scalar-associative & bspace X is scalar-unital )

proof

let a be Element of Z_2; :: according to VECTSP_1:def 14 :: thesis: for b₁, b₂ being Element of the carrier of (bspace X) holds a * (b₁ + b₂) = (a * b₁) + (a * b₂)
let x, y be Element of (bspace X); :: thesis: a * (x + y) = (a * x) + (a * y)
thus a * (x + y) = (a * x) + (a * y) by Th25; :: thesis: verum

end;

thus bspace X is scalar-distributive :: thesis: ( bspace X is scalar-associative & bspace X is scalar-unital )

proof

let a, b be Element of Z_2; :: according to VECTSP_1:def 15 :: thesis: for b₁ being Element of the carrier of (bspace X) holds (a + b) * b₁ = (a * b₁) + (b * b₁)
let x be Element of (bspace X); :: thesis: (a + b) * x = (a * x) + (b * x)
thus (a + b) * x = (a * x) + (b * x) by Th26; :: thesis: verum

end;

thus bspace X is scalar-associative :: thesis: bspace X is scalar-unital

proof

let a, b be Element of Z_2; :: according to VECTSP_1:def 16 :: thesis: for b₁ being Element of the carrier of (bspace X) holds (a * b) * b₁ = a * (b * b₁)
let x be Element of (bspace X); :: thesis: (a * b) * x = a * (b * x)
thus (a * b) * x = a * (b * x) by Th27; :: thesis: verum

end;

let x be Element of (bspace X); :: according to VECTSP_1:def 17 :: thesis: (1. Z_2) * x = x
thus (1. Z_2) * x = x by Th28; :: thesis: verum