let C be non empty set ; :: thesis: for f being PartFunc of C,COMPLEX holds |.f.| ^ = |.(f ^).|
let f be PartFunc of C,COMPLEX; :: thesis: |.f.| ^ = |.(f ^).|
A1: dom (|.f.| ^) = (dom |.f.|) \ (|.f.| " {0}) by RFUNCT_1:def 2
.= (dom f) \ (|.f.| " {0}) by VALUED_1:def 11
.= (dom f) \ (f " {0c}) by Th10
.= dom (f ^) by Def2
.= dom |.(f ^).| by VALUED_1:def 11 ;

now :: thesis: for c being Element of C st c in dom (|.f.| ^) holds
(|.f.| ^) . c = |.(f ^).| . c

let c be Element of C; :: thesis: ( c in dom (|.f.| ^) implies (|.f.| ^) . c = |.(f ^).| . c )
A2: dom f = dom |.f.| by VALUED_1:def 11;
assume A3: c in dom (|.f.| ^) ; :: thesis: (|.f.| ^) . c = |.(f ^).| . c
then A4: c in dom (f ^) by A1, VALUED_1:def 11;
c in (dom |.f.|) \ (|.f.| " {0}) by A3, RFUNCT_1:def 2;
then A5: c in dom |.f.| by XBOOLE_0:def 5;
thus (|.f.| ^) . c = (|.f.| . c) " by A3, RFUNCT_1:def 2
.= |.(f . c).| " by VALUED_1:18
.= |.(f /. c).| " by A5, A2, PARTFUN1:def 6
.= |.1r.| / |.(f /. c).| by COMPLEX1:48, XCMPLX_1:215
.= |.(1r / (f /. c)).| by COMPLEX1:67
.= |.((f /. c) ").| by COMPLEX1:def 4, XCMPLX_1:215
.= |.((f ^) /. c).| by A4, Def2
.= |.((f ^) . c).| by A4, PARTFUN1:def 6
.= |.(f ^).| . c by VALUED_1:18 ; :: thesis: verum

end;

hence |.f.| ^ = |.(f ^).| by A1, PARTFUN1:5; :: thesis: verum