for a1 being Element of COMPLEX
for y1 being FinSequence of COMPLEX
for a2 being Element of REAL
for y2 being FinSequence of REAL st a1 = a2 & y1 = y2 & len y1 = len y2 holds
(a1 multcomplex) * y1 = (a2 multreal) * y2