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