let X be set ; :: thesis: bspace X is VectSp-like
let a, b be Element of Z_2 ; :: according to VECTSP_1:def 26 :: thesis: for b₁, b₂ being Element of the carrier of (bspace X) holds
( a * (b₁ + b₂) = (a * b₁) + (a * b₂) & (a + b) * b₁ = (a * b₁) + (b * b₁) & (a * b) * b₁ = a * (b * b₁) & (1. Z_2 ) * b₁ = b₁ )
let x, y be Element of (bspace X); :: thesis: ( a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (1. Z_2 ) * x = x )
thus a * (x + y) = (a * x) + (a * y) by Th25; :: thesis: ( (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (1. Z_2 ) * x = x )
thus (a + b) * x = (a * x) + (b * x) by Th26; :: thesis: ( (a * b) * x = a * (b * x) & (1. Z_2 ) * x = x )
thus (a * b) * x = a * (b * x) by Th27; :: thesis: (1. Z_2 ) * x = x
thus (1. Z_2 ) * x = x by Th28; :: thesis: verum