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