:: deftheorem Def6 defines + QUATERNI:def 6 :
for x, y being Quaternion
for b₃ being Number holds
( b₃ = x + y iff ex x1, x2, x3, x4, y1, y2, y3, y4 being Real st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b₃ = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] ) );