let f, g be complex-valued Function; :: thesis: (f / g) (#) g = f | (dom (g ^ ))
A2: dom ((f / g) (#) g) = (dom (f / g)) /\ (dom g) by VALUED_1:def 4
.= ((dom f) /\ ((dom g) \ (g " {0 }))) /\ (dom g) by Def4
.= (dom f) /\ (((dom g) \ (g " {0 })) /\ (dom g)) by XBOOLE_1:16
.= (dom f) /\ ((dom (g ^ )) /\ (dom g)) by Def8
.= (dom f) /\ (dom (g ^ )) by Th11, XBOOLE_1:28
.= dom (f | (dom (g ^ ))) by RELAT_1:90 ;

now

let c be set ; :: thesis: ( c in dom ((f / g) (#) g) implies ((f / g) (#) g) . c = (f | (dom (g ^ ))) . c )
assume A3: c in dom ((f / g) (#) g) ; :: thesis: ((f / g) (#) g) . c = (f | (dom (g ^ ))) . c
then c in (dom f) /\ (dom (g ^ )) by A2, RELAT_1:90;
then A4: ( c in dom f & c in dom (g ^ ) ) by XBOOLE_0:def 4;
then A5: g . c <> 0 by Th13;
thus ((f / g) (#) g) . c = ((f / g) . c) * (g . c) by VALUED_1:5
.= ((f (#) (g ^ )) . c) * (g . c) by Th47
.= ((f . c) * ((g ^ ) . c)) * (g . c) by VALUED_1:5
.= ((f . c) * ((g . c) " )) * (g . c) by A4, Def8
.= (f . c) * (((g . c) " ) * (g . c))
.= (f . c) * 1 by A5, XCMPLX_0:def 7
.= (f | (dom (g ^ ))) . c by A2, A3, FUNCT_1:70 ; :: thesis: verum

end;

hence (f / g) (#) g = f | (dom (g ^ )) by A2, FUNCT_1:9; :: thesis: verum