ex x1, x2, x3, x4, y1, y2, y3, y4 being Real st
( z = [*x1,x2,x3,x4*] & z9 = [*y1,y2,y3,y4*] & z + z9 = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] ) by Def6;
hence z + z9 is quaternion ; :: thesis: verum