<k> *' = [*0 ,0 ,0 ,(- 1)*] by Th31, Th43;
hence ( Rea (<k> *' ) = 0 & Im1 (<k> *' ) = 0 & Im2 (<k> *' ) = 0 & Im3 (<k> *' ) = - 1 ) by Th23; :: thesis: verum