let c be Quaternion; :: thesis: 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; :: thesis: verum