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:217
.= abs (1 / (f . c)) by COMPLEX1:166
.= abs ((f . c) " ) by XCMPLX_1:217
.= 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:9; :: thesis: verum