let n be Element of NAT ; :: thesis: for c being Element of COMPLEX
for z being Element of COMPLEX n holds |.(c * z).| = |.c.| * |.z.|
let c be Element of COMPLEX ; :: thesis: for z being Element of COMPLEX n holds |.(c * z).| = |.c.| * |.z.|
let z be Element of COMPLEX n; :: thesis: |.(c * z).| = |.c.| * |.z.|
A1: ( 0 <= |.c.| ^2 & 0 <= Sum (sqr (abs z)) ) by RVSUM_1:116, XREAL_1:65;
thus |.(c * z).| = sqrt (Sum (sqr (|.c.| * (abs z)))) by Th62
.= sqrt (Sum ((|.c.| ^2 ) * (sqr (abs z)))) by RVSUM_1:84
.= sqrt ((|.c.| ^2 ) * (Sum (sqr (abs z)))) by RVSUM_1:117
.= (sqrt (|.c.| ^2 )) * (sqrt (Sum (sqr (abs z)))) by A1, SQUARE_1:97
.= |.c.| * |.z.| by COMPLEX1:132, SQUARE_1:89 ; :: thesis: verum