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