assume that
A3: x = a and
A4: y = b ; :: thesis: x * y = a * b
reconsider a9 = a, b9 = b as Element of QUATERNION by QUATERNI:def 2;
thus x * y = multquaternion . (a9,b9) by A3, A4, Def10
.= a * b by Def6 ; :: thesis: verum