theorem :: LOPBAN15:5

for v being Element of RNS_Real
for v1 being Element of REAL
for a being Real st v = v1 holds
a * v = a * v1 by BINOP_2:def 11;