set V = StructVectSp K;

now

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 v' = v, w' = w as Element of K ;
A1: the lmult of (StructVectSp K) . x,w = x * w by VECTSP_1:def 24;
A2: the lmult of (StructVectSp K) . y,v = y * v by VECTSP_1:def 24;
thus x * (v + w) = x * (v' + w') by VECTSP_1:def 24
.= (x * v') + (x * w') by VECTSP_1:def 18
.= (x * v) + (x * w) by A1, VECTSP_1:def 24 ; :: thesis: ( (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. K) * v = v )
thus (x + y) * v = (x + y) * v' by VECTSP_1:def 24
.= (x * v') + (y * v') by VECTSP_1:def 18
.= (x * v) + (y * v) by A2, VECTSP_1:def 24 ; :: thesis: ( (x * y) * v = x * (y * v) & (1. K) * v = v )
thus (x * y) * v = (x * y) * v' by VECTSP_1:def 24
.= x * (y * v') by GROUP_1:def 4
.= the lmult of (StructVectSp K) . x,(y * v) by VECTSP_1:def 24
.= x * (y * v) by VECTSP_1:def 24 ; :: thesis: (1. K) * v = v
thus (1. K) * v = (1. K) * v' by VECTSP_1:def 24
.= v by VECTSP_1:def 19 ; :: thesis: verum

end;

hence StructVectSp K is VectSp-like by VECTSP_1:def 26; :: thesis: verum