let C be non empty set ; :: thesis: for f, g being PartFunc of C,COMPLEX holds f / g = f (#) (g ^)
let f, g be PartFunc of C,COMPLEX; :: thesis: f / g = f (#) (g ^)

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

let c be Element of C; :: thesis: ( c in dom (f / g) implies (f / g) /. c = (f (#) (g ^)) /. c )
assume A2: c in dom (f / g) ; :: thesis: (f / g) /. c = (f (#) (g ^)) /. c
then c in (dom f) /\ ((dom g) \ (g " {0c})) by Def1;
then A3: c in (dom f) /\ (dom (g ^)) by Def2;
then A4: c in dom (g ^) by XBOOLE_0:def 4;
A5: c in dom (f (#) (g ^)) by A3, Th3;
thus (f / g) /. c = (f /. c) * ((g /. c) ") by A2, Def1
.= (f /. c) * ((g ^) /. c) by A4, Def2
.= (f (#) (g ^)) /. c by A5, Th3 ; :: thesis: verum

end;

dom (f / g) = (dom f) /\ ((dom g) \ (g " {0c})) by Def1
.= (dom f) /\ (dom (g ^)) by Def2
.= dom (f (#) (g ^)) by Th3 ;
hence f / g = f (#) (g ^) by A1, PARTFUN2:1; :: thesis: verum