set V = StructVectSp K;

now

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 by RLVECT_1:def 4; :: thesis: verum