let c be quaternion number ; :: thesis: c + 0q = c
A1: 0q = [*0 ,0 *] by ARYTM_0:def 7
.= [*0 ,0 ,0 ,0 *] by QUATERNI:def 6, QUATERNI:91 ;
consider x, y, w, z being Element of REAL such that
A2: c = [*x,y,w,z*] by QUA7;
c + 0q = [*(x + 0 ),(y + 0 ),(w + 0 ),(z + 0 )*] by A1, A2, QUATERNI:def 7
.= [*x,y,w,z*] ;
hence c + 0q = c by A2; :: thesis: verum