let n be Element of NAT ; :: thesis: for z being Element of COMPLEX n holds abs (- z) = abs z
let z be Element of COMPLEX n; :: thesis: abs (- z) = abs z

now

let j be Nat; :: thesis: ( j in Seg n implies (abs (- z)) . j = (abs z) . j )
assume A1: j in Seg n ; :: thesis: (abs (- z)) . j = (abs z) . j
then reconsider c = z . j, c9 = (- z) . j as Element of COMPLEX by Th21;
thus (abs (- z)) . j = |.c9.| by A1, Th59
.= |.(- c).| by A1, Th29
.= |.c.| by COMPLEX1:138
.= (abs z) . j by A1, Th59 ; :: thesis: verum

end;

hence abs (- z) = abs z by FINSEQ_2:139; :: thesis: verum