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

let x be set ; :: 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 = abs ((- f) . x) by VALUED_1:18
.= abs (- (f . x)) by VALUED_1:8
.= abs (f . x) by COMPLEX1:138
.= (abs f) . x by VALUED_1:18 ; :: thesis: verum

end;

hence abs (- f) = abs f by a1, a2, a3, FUNCT_1:9; :: thesis: verum