theorem :: REAL_NS3:17

for n being Nat
for a being Element of REAL
for a1 being Element of F_Real
for x, y being Element of REAL n
for x1, y1 being Element of n -tuples_on the carrier of F_Real st a = a1 & x = x1 & y = y1 holds
( a * x = a1 * x1 & x + y = x1 + y1 ) ;