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

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

let c be object ; :: 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, Def2
.= |.(f . c).| " by VALUED_1:18
.= 1 / |.(f . c).| by XCMPLX_1:215
.= |.(1 / (f . c)).| by COMPLEX1:80
.= |.((f . c) ").| by XCMPLX_1:215
.= |.((f ^) . c).| by A3, Def2
.= (abs (f ^)) . c by VALUED_1:18 ; :: thesis: verum

end;

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