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

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, Th5;
thus (f / g) /. c = (f /. c) * ((g /. c) " ) by A2, Def1
.= (f /. c) * ((g ^ ) /. c) by A4, Def2
.= (f (#) (g ^ )) /. c by A5, Th5 ; :: thesis: verum

end;

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