let z be Quaternion; :: thesis: z - 0q = z
consider x, y, w, v being Real such that
A1: z = [*x,y,w,v*] by QUATERNI:7;
0q = [*(In (0,REAL)),(In (0,REAL))*] by ARYTM_0:def 5
.= [*0,0,0,0*] by QUATERNI:91 ;
then - 0q = [*(- 0),(- 0),(- 0),(- 0)*] by QUATERN2:4;
then z - 0q = [*(x + (- 0)),(y + (- 0)),(w + (- 0)),(v + (- 0))*] by A1, QUATERNI:def 7
.= [*x,y,w,v*] ;
hence z - 0q = z by A1; :: thesis: verum