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 = addquaternion . a',b' by Z, Def11
.= a + b by Def6 ; :: thesis: verum