let n be 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 :: thesis: for j being Nat st j in Seg n holds
(abs (c * z)) . j = (|.c.| * (abs z)) . j

let j be Nat; :: thesis: ( j in Seg n implies (abs (c * z)) . j = (|.c.| * (abs z)) . j )
reconsider w = j as Element of NAT by ORDINAL1:def 12;
assume A1: j in Seg n ; :: thesis: (abs (c * z)) . j = (|.c.| * (abs z)) . j
then reconsider c9 = z . j, cc = (c * z) . j as Element of COMPLEX by Th57;
reconsider ac = (abs z) . w as Real ;
thus (abs (c * z)) . j = |.cc.| by A1, Th88
.= |.(c * c9).| by A1, Th81
.= |.c.| * |.c9.| by COMPLEX1:65
.= |.c.| * ac by A1, Th88
.= (|.c.| * (abs z)) . j by RVSUM_1:45 ; :: thesis: verum

end;

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