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