let n be 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 :: thesis: for j being Nat st j in Seg n holds
(abs (- z)) . j = (abs z) . j
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 Th57;
thus (abs (- z)) . j = |.c9.| by A1, Th88
.= |.(- c).| by A1, Th60
.= |.c.| by COMPLEX1:52
.= (abs z) . j by A1, Th88 ; :: thesis: verum
end;
hence abs (- z) = abs z by FINSEQ_2:119; :: thesis: verum