let f be complex-valued Function; :: thesis: (abs f) ^ = abs (f ^)
A1: dom ((abs f) ^) = (dom (abs f)) \ ((abs f) " {0}) by Def8
.= (dom f) \ ((abs f) " {0}) by VALUED_1:def 11
.= (dom f) \ (f " {0}) by Th15
.= dom (f ^) by Def8
.= dom (abs (f ^)) by VALUED_1:def 11 ;

now

let c be set ; :: thesis: ( c in dom ((abs f) ^) implies ((abs f) ^) . c = (abs (f ^)) . c )
assume A2: c in dom ((abs f) ^) ; :: thesis: ((abs f) ^) . c = (abs (f ^)) . c
then A3: c in dom (f ^) by A1, VALUED_1:def 11;
thus ((abs f) ^) . c = ((abs f) . c) " by A2, Def8
.= (abs (f . c)) " by VALUED_1:18
.= 1 / (abs (f . c)) by XCMPLX_1:215
.= abs (1 / (f . c)) by COMPLEX1:80
.= abs ((f . c) ") by XCMPLX_1:215
.= abs ((f ^) . c) by A3, Def8
.= (abs (f ^)) . c by VALUED_1:18 ; :: thesis: verum

end;

hence (abs f) ^ = abs (f ^) by A1, FUNCT_1:2; :: thesis: verum