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 )
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 8;
then A5: c in dom |.f.| by XBOOLE_0:def 5;
thus (|.f.| ^ ) . c = (|.f.| . c) " by A3, RFUNCT_1:def 8
.= |.(f . c).| " by VALUED_1:18
.= |.(f /. c).| " by A5, A2, 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