let z be Quaternion; :: thesis: z *' = [*(Rea z),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*]
<i> = [*zz,jj,zz,zz*] by Lm2, Lm3;
then z *' = (((Rea z) + [*((- (Im1 z)) * 0),((- (Im1 z)) * 1),((- (Im1 z)) * 0),((- (Im1 z)) * 0)*]) + ((- (Im2 z)) * <j>)) + ((- (Im3 z)) * <k>) by Def20
.= (((Rea z) + [*0,(- (Im1 z)),0,0*]) + [*((- (Im2 z)) * 0),((- (Im2 z)) * 0),((- (Im2 z)) * 1),((- (Im2 z)) * 0)*]) + ((- (Im3 z)) * <k>) by Def20
.= (((Rea z) + [*0,(- (Im1 z)),0,0*]) + [*0,0,(- (Im2 z)),0*]) + [*((- (Im3 z)) * 0),((- (Im3 z)) * 0),((- (Im3 z)) * 0),((- (Im3 z)) * 1)*] by Def20
.= ([*((Rea z) + 0),(- (Im1 z)),0,0*] + [*0,0,(- (Im2 z)),0*]) + [*0,0,0,(- (Im3 z))*] by Def18
.= [*((Rea z) + 0),((- (Im1 z)) + 0),(0 + (- (Im2 z))),(0 + 0)*] + [*0,0,0,(- (Im3 z))*] by Def6
.= [*((Rea z) + 0),((- (Im1 z)) + 0),((- (Im2 z)) + 0),(0 + (- (Im3 z)))*] by Def6 ;
hence z *' = [*(Rea z),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] ; :: thesis: verum