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 8
.= (dom f) \ (|.f.| " {0 }) by VALUED_1:def 11
.= (dom f) \ (f " {0c }) by Th19
.= dom (f ^ ) by Def2
.= dom |.(f ^ ).| by VALUED_1:def 11 ;

now

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

end;

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