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