set V = StructVectSp K;
now :: thesis: for x, y being Vector of (StructVectSp K) holds x + y = y + x
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 ; :: thesis: verum