let z be quaternion number ; :: thesis: Im1 z <= |.z.|
0 <= (Im1 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 Lm24, 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 - (Im1 z) <= |.z.| by A1, SQUARE_1:90;
hence Im1 z <= |.z.| by A2; :: thesis: verum

end;

end;