assume Z: ( x = a & y = b ) ; :: thesis: x * y = a * b
reconsider a' = a, b' = b as Element of QUATERNION by QUATERNI:def 2;
thus x * y = multquaternion . a',b' by Z, Def11
.= a * b by Def8 ; :: thesis: verum