[*zz,jj*] = [*0,1,0,0*] by Lm3;
hence ( Rea <i> = 0 & Im1 <i> = 1 & Im2 <i> = 0 & Im3 <i> = 0 ) by Lm2, Th16; :: thesis: verum