:: deftheorem Def20 defines * QUATERNI:def 20 :
for x being Real
for y being Quaternion
for b₃ being Number holds
( b₃ = x * y iff ex y1, y2, y3, y4 being Real st
( y = [*y1,y2,y3,y4*] & b₃ = [*(x * y1),(x * y2),(x * y3),(x * y4)*] ) );