assume that
A1: x = a and
A2: y = b ; :: thesis: x + y = a + b
reconsider a9 = a, b9 = b as Element of QUATERNION by QUATERNI:def 2;
thus x + y = addquaternion . (a9,b9) by A1, A2, Def10
.= a + b by Def4 ; :: thesis: verum