set V = StructVectSp K;

now :: thesis: for x, y being Element of K
for v, w being Vector of (StructVectSp K) holds
( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. K) * v = v )

let x, y be Element of K; :: thesis: for v, w being Vector of (StructVectSp K) holds
( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. K) * v = v )
let v, w be Vector of (StructVectSp K); :: thesis: ( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. K) * v = v )
reconsider v9 = v, w9 = w as Element of K ;
thus x * (v + w) = x * (v9 + w9)
.= (x * v9) + (x * w9) by VECTSP_1:def 7
.= (x * v) + (x * w) ; :: thesis: ( (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. K) * v = v )
thus (x + y) * v = (x + y) * v9
.= (x * v9) + (y * v9) by VECTSP_1:def 7
.= (x * v) + (y * v) ; :: thesis: ( (x * y) * v = x * (y * v) & (1. K) * v = v )
thus (x * y) * v = (x * y) * v9
.= x * (y * v9) by GROUP_1:def 3
.= the lmult of (StructVectSp K) . (x,(y * v))
.= x * (y * v) ; :: thesis: (1. K) * v = v
thus (1. K) * v = (1. K) * v9
.= v ; :: thesis: verum

end;

hence ( StructVectSp K is vector-distributive & StructVectSp K is scalar-distributive & StructVectSp K is scalar-associative & StructVectSp K is scalar-unital ) ; :: thesis: verum