thus (1. R) ^2 = (1. R) * (1. R) by O_RING_1:def 1
.= 1. R ; :: thesis: verum