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

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

let c be Element of C; :: thesis: ( c in dom ((f / g) (#) (f1 / g1)) implies ((f / g) (#) (f1 / g1)) /. c = ((f (#) f1) / (g (#) g1)) /. c )
assume A2: c in dom ((f / g) (#) (f1 / g1)) ; :: thesis: ((f / g) (#) (f1 / g1)) /. c = ((f (#) f1) / (g (#) g1)) /. c
then c in (dom (f / g)) /\ (dom (f1 / g1)) by Th3;
then A3: c in (dom (f (#) (g ^))) /\ (dom (f1 / g1)) by Th38;
then A4: c in dom (f (#) (g ^)) by XBOOLE_0:def 4;
then A5: c in (dom f) /\ (dom (g ^)) by Th3;
c in (dom (f (#) (g ^))) /\ (dom (f1 (#) (g1 ^))) by A3, Th38;
then A6: c in dom (f1 (#) (g1 ^)) by XBOOLE_0:def 4;
then A7: c in (dom f1) /\ (dom (g1 ^)) by Th3;
then A8: c in dom f1 by XBOOLE_0:def 4;
c in dom f by A5, XBOOLE_0:def 4;
then c in (dom f) /\ (dom f1) by A8, XBOOLE_0:def 4;
then A9: c in dom (f (#) f1) by Th3;
A10: c in dom (g1 ^) by A7, XBOOLE_0:def 4;
c in dom (g ^) by A5, XBOOLE_0:def 4;
then c in (dom (g ^)) /\ (dom (g1 ^)) by A10, XBOOLE_0:def 4;
then A11: c in dom ((g ^) (#) (g1 ^)) by Th3;
then c in dom ((g (#) g1) ^) by Th34;
then c in (dom (f (#) f1)) /\ (dom ((g (#) g1) ^)) by A9, XBOOLE_0:def 4;
then A12: c in dom ((f (#) f1) (#) ((g (#) g1) ^)) by Th3;
thus ((f / g) (#) (f1 / g1)) /. c = ((f / g) /. c) * ((f1 / g1) /. c) by A2, Th3
.= ((f (#) (g ^)) /. c) * ((f1 / g1) /. c) by Th38
.= ((f (#) (g ^)) /. c) * ((f1 (#) (g1 ^)) /. c) by Th38
.= ((f /. c) * ((g ^) /. c)) * ((f1 (#) (g1 ^)) /. c) by A4, Th3
.= ((f /. c) * ((g ^) /. c)) * ((f1 /. c) * ((g1 ^) /. c)) by A6, Th3
.= (f /. c) * ((f1 /. c) * (((g ^) /. c) * ((g1 ^) /. c)))
.= (f /. c) * ((f1 /. c) * (((g ^) (#) (g1 ^)) /. c)) by A11, Th3
.= ((f /. c) * (f1 /. c)) * (((g ^) (#) (g1 ^)) /. c)
.= ((f /. c) * (f1 /. c)) * (((g (#) g1) ^) /. c) by Th34
.= ((f (#) f1) /. c) * (((g (#) g1) ^) /. c) by A9, Th3
.= ((f (#) f1) (#) ((g (#) g1) ^)) /. c by A12, Th3
.= ((f (#) f1) / (g (#) g1)) /. c by Th38 ; :: thesis: verum

end;

dom ((f / g) (#) (f1 / g1)) = (dom (f / g)) /\ (dom (f1 / g1)) by Th3
.= ((dom f) /\ ((dom g) \ (g " {0c}))) /\ (dom (f1 / g1)) by Def1
.= ((dom f) /\ ((dom g) \ (g " {0c}))) /\ ((dom f1) /\ ((dom g1) \ (g1 " {0c}))) by Def1
.= (dom f) /\ (((dom g) \ (g " {0c})) /\ ((dom f1) /\ ((dom g1) \ (g1 " {0c})))) by XBOOLE_1:16
.= (dom f) /\ ((dom f1) /\ (((dom g) \ (g " {0c})) /\ ((dom g1) \ (g1 " {0c})))) by XBOOLE_1:16
.= ((dom f) /\ (dom f1)) /\ (((dom g) \ (g " {0c})) /\ ((dom g1) \ (g1 " {0c}))) by XBOOLE_1:16
.= (dom (f (#) f1)) /\ (((dom g) \ (g " {0c})) /\ ((dom g1) \ (g1 " {0c}))) by Th3
.= (dom (f (#) f1)) /\ ((dom (g (#) g1)) \ ((g (#) g1) " {0c})) by Th7
.= dom ((f (#) f1) / (g (#) g1)) by Def1 ;
hence (f / g) (#) (f1 / g1) = (f (#) f1) / (g (#) g1) by A1, PARTFUN2:1; :: thesis: verum