assume that
A1: x = y and
A2: a = b ; :: thesis: a * x = b * y
reconsider y1 = y as Element of REAL n by A1, REAL_NS1:def 6;
thus a * x = (Euclid_mult n) . (b,y1) by A1, A2, REAL_NS1:def 6
.= b (#) y by REAL_NS1:def 2 ; :: thesis: verum