theorem :: LOPBAN15:6

for v being Element of RNS_Real
for v1 being Element of REAL st v = v1 holds
||.v.|| = |.v1.| by EUCLID:def 2;