let n be 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:86, XREAL_1:63;
thus |.(c * z).| = sqrt (Sum (sqr (|.c.| * (abs z)))) by Th91
.= sqrt (Sum ((|.c.| ^2) * (sqr (abs z)))) by RVSUM_1:58
.= sqrt ((|.c.| ^2) * (Sum (sqr (abs z)))) by RVSUM_1:87
.= (sqrt (|.c.| ^2)) * (sqrt (Sum (sqr (abs z)))) by A1, SQUARE_1:29
.= |.c.| * |.z.| by COMPLEX1:46, SQUARE_1:22 ; :: thesis: verum