[*1,0,0,0*] = [*jj,zz*] by Lm3;
hence [*jj,zz,zz,zz*] = 1 by ARYTM_0:def 5; :: thesis: verum