ex y1, y2, y3, y4 being Element of REAL st
( z' = [*y1,y2,y3,y4*] & x + z' = [*(x + y1),y2,y3,y4*] ) by Def19;
hence x + z' is quaternion ; :: thesis: verum