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: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