let A be Element of R; :: thesis: (R,A,A)
A * (1. R) = A by VECTSP_1:def 4;
hence (R,A,A) by Def1; :: thesis: verum