set V = StructVectSp K;

now

let x, y, z be Vector of (StructVectSp K); :: thesis: (x + y) + z = x + (y + z)
reconsider x9 = x, y9 = y, z9 = z as Element of K ;
thus (x + y) + z = (x9 + y9) + z9
.= x9 + (y9 + z9) by RLVECT_1:def 3
.= x + (y + z) ; :: thesis: verum

end;

hence StructVectSp K is add-associative by RLVECT_1:def 3; :: thesis: verum