set V = StructVectSp K;

now

let x, y, z be Vector of ; :: thesis: (x + y) + z = x + (y + z)
reconsider x' = x, y' = y, z' = z as Element of ;
thus (x + y) + z = (x' + y') + z'
.= x' + (y' + z') by RLVECT_1:def 6
.= x + (y + z) ; :: thesis: verum

end;

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