let z1, z2 be quaternion number ; :: thesis: ( |.z1.| - |.z2.| <> 0 implies ((|.z1.| ^2 ) + (|.z2.| ^2 )) - ((2 * |.z1.|) * |.z2.|) > 0 )
assume A1: |.z1.| - |.z2.| <> 0 ; :: thesis: ((|.z1.| ^2 ) + (|.z2.| ^2 )) - ((2 * |.z1.|) * |.z2.|) > 0
(|.z1.| - |.z2.|) ^2 > 0 by A1, SQUARE_1:74;
hence ((|.z1.| ^2 ) + (|.z2.| ^2 )) - ((2 * |.z1.|) * |.z2.|) > 0 ; :: thesis: verum