let c be Quaternion; c + 0q = c
A1: 0q =
[*(In (0,REAL)),(In (0,REAL))*]
by ARYTM_0:def 5
.=
[*0,0,0,0*]
by Lm3
;
consider x, y, w, z being Real such that
A2:
c = [*x,y,w,z*]
by Th2;
c + 0q =
[*(x + 0),(y + 0),(w + 0),(z + 0)*]
by A1, A2, Def6
.=
[*x,y,w,z*]
;
hence
c + 0q = c
by A2; verum