set V = StructVectSp K;

now

let x, y be Vector of ; :: thesis: x + y = y + x
reconsider x' = x, y' = y as Element of ;
thus x + y = y' + x' by RLVECT_1:5
.= y + x ; :: thesis: verum

end;

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