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