set V = R ^* n;

now :: thesis: for x being Vector of (R ^* n) holds (1. R) * x = x

let x be Vector of (R ^* n); :: thesis: (1. R) * x = x
reconsider u = x as Element of n -tuples_on the carrier of R by DEF;
thus (1. R) * x = the lmult of (R ^* n) . ((1. R),u) by VECTSP_1:def 12
.= (vector_mult (n,R)) . ((1. R),u) by DEF
.= (1. R) * u by Defm
.= x by FVSUM_1:57 ; :: thesis: verum

end;

hence R ^* n is scalar-unital by VECTSP_1:def 17; :: thesis: verum