take
[*(x * y1),(x * y2),(x * y3),(x * y4)*]
; ex y1, y2, y3, y4 being Real st
( y = [*y1,y2,y3,y4*] & [*(x * y1),(x * y2),(x * y3),(x * y4)*] = [*(x * y1),(x * y2),(x * y3),(x * y4)*] )
thus
ex y1, y2, y3, y4 being Real st
( y = [*y1,y2,y3,y4*] & [*(x * y1),(x * y2),(x * y3),(x * y4)*] = [*(x * y1),(x * y2),(x * y3),(x * y4)*] )
by A1; verum