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