let z be quaternion number ; :: thesis: z - 0q = z
0q = [*0 ,0 *] by ARYTM_0:def 7
.= [*0 ,0 ,0 ,0 *] by QUATERNI:91 ;
then A1: - 0q = [*(- 0 ),(- 0 ),(- 0 ),(- 0 )*] by QUATERN2:4;
z in QUATERNION by QUATERNI:def 2;
then consider x, y, w, v being Element of REAL such that
A2: z = [*x,y,w,v*] by QUATERNI:7;
z - 0q = [*(x + (- 0 )),(y + (- 0 )),(w + (- 0 )),(v + (- 0 ))*] by A1, A2, QUATERNI:def 7
.= [*x,y,w,v*] ;
hence z - 0q = z by A2; :: thesis: verum