set V = StructVectSp K;

now :: thesis: for x being Vector of (StructVectSp K) holds x + (0. (StructVectSp K)) = x

let x be Vector of (StructVectSp K); :: thesis: x + (0. (StructVectSp K)) = x
reconsider x9 = x as Element of K ;
thus x + (0. (StructVectSp K)) = x9 + (0. K)
.= x by RLVECT_1:def 4 ; :: thesis: verum

end;

hence StructVectSp K is right_zeroed ; :: thesis: verum