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