ex y1, y2, y3, y4 being Element of REAL st
( z9 = [*y1,y2,y3,y4*] & x * z9 = [*(x * y1),(x * y2),(x * y3),(x * y4)*] ) by Def21;
hence x * z9 in QUATERNION ; :: according to QUATERNI:def 2 :: thesis: verum