set V = StructVectSp K;

now :: thesis: for x, y, z being Vector of (StructVectSp K) holds (x + y) + z = x + (y + z)

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 ; :: thesis: verum