let C be non empty set ; :: thesis: for f, g being PartFunc of C,COMPLEX holds (f / g) (#) g = f | (dom (g ^))
let f, g be PartFunc of C,COMPLEX; :: thesis: (f / g) (#) g = f | (dom (g ^))
A1: dom ((f / g) (#) g) = (dom (f / g)) /\ (dom g) by Th3
.= ((dom f) /\ ((dom g) \ (g " {0c}))) /\ (dom g) by Def1
.= (dom f) /\ (((dom g) \ (g " {0c})) /\ (dom g)) by XBOOLE_1:16
.= (dom f) /\ ((dom (g ^)) /\ (dom g)) by Def2
.= (dom f) /\ (dom (g ^)) by Th6, XBOOLE_1:28
.= dom (f | (dom (g ^))) by RELAT_1:61 ;

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

let c be Element of C; :: thesis: ( c in dom ((f / g) (#) g) implies ((f / g) (#) g) /. c = (f | (dom (g ^))) /. c )
assume A2: c in dom ((f / g) (#) g) ; :: thesis: ((f / g) (#) g) /. c = (f | (dom (g ^))) /. c
then A3: c in (dom f) /\ (dom (g ^)) by A1, RELAT_1:61;
then A4: c in dom (f (#) (g ^)) by Th3;
A5: c in dom (g ^) by A3, XBOOLE_0:def 4;
then A6: g /. c <> 0c by Th8;
thus ((f / g) (#) g) /. c = ((f / g) /. c) * (g /. c) by A2, Th3
.= ((f (#) (g ^)) /. c) * (g /. c) by Th38
.= ((f /. c) * ((g ^) /. c)) * (g /. c) by A4, Th3
.= ((f /. c) * ((g /. c) ")) * (g /. c) by A5, Def2
.= (f /. c) * (((g /. c) ") * (g /. c))
.= (f /. c) * 1r by A6, COMPLEX1:def 4, XCMPLX_0:def 7
.= (f | (dom (g ^))) /. c by A1, A2, COMPLEX1:def 4, PARTFUN2:15 ; :: thesis: verum

end;

hence (f / g) (#) g = f | (dom (g ^)) by A1, PARTFUN2:1; :: thesis: verum