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 ;

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

hence
(abs f) ^ = abs (f ^)
by A1, FUNCT_1:2; :: thesis: verum((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;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