let n be Element of NAT ; :: thesis: for c being Element of COMPLEX
for z being Element of COMPLEX n holds abs (c * z) = |.c.| * (abs z)
let c be Element of COMPLEX ; :: thesis: for z being Element of COMPLEX n holds abs (c * z) = |.c.| * (abs z)
let z be Element of COMPLEX n; :: thesis: abs (c * z) = |.c.| * (abs z)

now

let j be Nat; :: thesis: ( j in Seg n implies (abs (c * z)) . j = (|.c.| * (abs z)) . j )
assume A1: j in Seg n ; :: thesis: (abs (c * z)) . j = (|.c.| * (abs z)) . j
then reconsider c' = z . j, cc = (c * z) . j as Element of COMPLEX by Th21;
reconsider w = j as Element of NAT by ORDINAL1:def 13;
len (abs z) = n by FINSEQ_1:def 18;
then Seg n = dom (abs z) by FINSEQ_1:def 3;
then reconsider ac = (abs z) . w as Real by A1, FINSEQ_2:13;
thus (abs (c * z)) . j = |.cc.| by A1, Th59
.= |.(c * c').| by A1, Th52
.= |.c.| * |.c'.| by COMPLEX1:151
.= |.c.| * ac by A1, Th59
.= (|.c.| * (abs z)) . j by RVSUM_1:67 ; :: thesis: verum

end;

hence abs (c * z) = |.c.| * (abs z) by FINSEQ_2:139; :: thesis: verum