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 ^ ))
A2: dom ((f / g) (#) g) = (dom (f / g)) /\ (dom g) by Th5
.= ((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 Th15, XBOOLE_1:28
.= dom (f | (dom (g ^ ))) by RELAT_1:90 ;

now

let c be Element of C; :: 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 A4: c in (dom f) /\ (dom (g ^ )) by A2, RELAT_1:90;
then A5: c in dom (f (#) (g ^ )) by Th5;
A6: ( c in dom f & c in dom (g ^ ) ) by A4, XBOOLE_0:def 4;
then A7: g /. c <> 0c by Th17;
thus ((f / g) (#) g) /. c = ((f / g) /. c) * (g /. c) by A3, Th5
.= ((f (#) (g ^ )) /. c) * (g /. c) by Th51
.= ((f /. c) * ((g ^ ) /. c)) * (g /. c) by A5, Th5
.= ((f /. c) * ((g /. c) " )) * (g /. c) by A6, Def2
.= (f /. c) * (((g /. c) " ) * (g /. c))
.= (f /. c) * 1r by A7, COMPLEX1:def 7, XCMPLX_0:def 7
.= (f | (dom (g ^ ))) /. c by A2, A3, COMPLEX1:def 7, PARTFUN2:32 ; :: thesis: verum

end;

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