set V = StructVectSp K;

now

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

end;

hence StructVectSp K is Abelian by RLVECT_1:def 2; :: thesis: verum