let a be Real; :: thesis: for z being Complex st 0 <= a & a <= 1 holds
( |.(a * z).| = a * |.z.| & |.((1r - a) * z).| = (1r - a) * |.z.| )
let z be Complex; :: thesis: ( 0 <= a & a <= 1 implies ( |.(a * z).| = a * |.z.| & |.((1r - a) * z).| = (1r - a) * |.z.| ) )
assume that
A1: 0 <= a and
A2: a <= 1 ; :: thesis: ( |.(a * z).| = a * |.z.| & |.((1r - a) * z).| = (1r - a) * |.z.| )
A3: |.((1r - a) * z).| = |.(1r - a).| * |.z.| by COMPLEX1:65
.= (1r - a) * |.z.| by A2, COMPLEX1:43, XREAL_1:48 ;
|.(a * z).| = |.a.| * |.z.| by COMPLEX1:65
.= a * |.z.| by A1, COMPLEX1:43 ;
hence ( |.(a * z).| = a * |.z.| & |.((1r - a) * z).| = (1r - a) * |.z.| ) by A3; :: thesis: verum