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