for X being set holds
( bspace X is vector-distributive & bspace X is scalar-distributive & bspace X is scalar-associative & bspace X is scalar-unital ) by Th25, Th26, Th27, Th28;