ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL st
( z = [*x1,x2,x3,x4*] & z' = [*y1,y2,y3,y4*] & z + z' = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] ) by Def7;
hence z + z' in QUATERNION ; :: according to QUATERNI:def 2 :: thesis: verum