[*jj,zz*] = [*1,0,0,0*] by Lm3;
then A1: 1q = [*1,0,0,0*] by ARYTM_0:def 5;
A2: Rea [*jj,zz,zz,zz*] = 1 by Th16;
A3: Im1 [*jj,zz,zz,zz*] = 0 by Th16;
A4: Im2 [*jj,zz,zz,zz*] = 0 by Th16;
Im3 [*jj,zz,zz,zz*] = 0 by Th16;
hence 1q *' = 1q by A1, A2, A3, A4, Th36; :: thesis: verum