let f be complex-valued Function; :: thesis: abs (- f) = abs f
A1: dom (abs (- f)) = dom (- f) by VALUED_1:def 11;
A2: dom (abs f) = dom f by VALUED_1:def 11;
A3: dom (- f) = dom f by VALUED_1:8;

now :: thesis: for x being object st x in dom (abs (- f)) holds
(abs (- f)) . x = (abs f) . x

let x be object ; :: thesis: ( x in dom (abs (- f)) implies (abs (- f)) . x = (abs f) . x )
assume x in dom (abs (- f)) ; :: thesis: (abs (- f)) . x = (abs f) . x
thus (abs (- f)) . x = |.((- f) . x).| by VALUED_1:18
.= |.(- (f . x)).| by VALUED_1:8
.= |.(f . x).| by COMPLEX1:52
.= (abs f) . x by VALUED_1:18 ; :: thesis: verum

end;

hence abs (- f) = abs f by A1, A2, A3, FUNCT_1:2; :: thesis: verum