take [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] ; :: thesis: ex x1, x2, x3, x4, y1, y2, y3, y4 being Real st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] )
thus ex x1, x2, x3, x4, y1, y2, y3, y4 being Real st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] ) by A1, A2; :: thesis: verum