let z be quaternion number ; :: thesis: Im1 z <= |.z.|
( 0 <= (Rea z) ^2 & 0 <= (Im1 z) ^2 & 0 <= (Im2 z) ^2 & 0 <= (Im3 z) ^2 ) by XREAL_1:65;
then A1: sqrt ((Im1 z) ^2 ) <= sqrt (((((Rea z) ^2 ) + ((Im1 z) ^2 )) + ((Im2 z) ^2 )) + ((Im3 z) ^2 )) by Lm22, SQUARE_1:94;

per cases ( Im1 z >= 0 or Im1 z < 0 ) ;

suppose Im1 z >= 0 ; :: thesis: Im1 z <= |.z.|

hence Im1 z <= |.z.| by A1, SQUARE_1:89; :: thesis: verum

end;

suppose A2: Im1 z < 0 ; :: thesis: Im1 z <= |.z.|

then A3: - (Im1 z) <= |.z.| by A1, SQUARE_1:90;
0 * (- 1) < (Im1 z) * (- 1) by A2, XREAL_1:71;
hence Im1 z <= |.z.| by A3; :: thesis: verum

end;

end;