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