let a be real number ; :: thesis: for z being complex number st 0 <= a & a <= 1 holds
( |.(a * z).| = a * |.z.| & |.((1r - a) * z).| = (1r - a) * |.z.| )
let z be complex number ; :: thesis: ( 0 <= a & a <= 1 implies ( |.(a * z).| = a * |.z.| & |.((1r - a) * z).| = (1r - a) * |.z.| ) )
assume A1: ( 0 <= a & a <= 1 ) ; :: thesis: ( |.(a * z).| = a * |.z.| & |.((1r - a) * z).| = (1r - a) * |.z.| )
A2: 1 - a >= 0 by A1, XREAL_1:50;
A3: |.(a * z).| = |.a.| * |.z.| by COMPLEX1:151
.= a * |.z.| by A1, COMPLEX1:129 ;
|.((1r - a) * z).| = |.(1r - a).| * |.z.| by COMPLEX1:151
.= (1r - a) * |.z.| by A2, COMPLEX1:129 ;
hence ( |.(a * z).| = a * |.z.| & |.((1r - a) * z).| = (1r - a) * |.z.| ) by A3; :: thesis: verum