let C be non empty set ; 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; (f / g) (#) (f1 / g1) = (f (#) f1) / (g (#) g1)
A1:
now for c being Element of C st c in dom ((f / g) (#) (f1 / g1)) holds
((f / g) (#) (f1 / g1)) /. c = ((f (#) f1) / (g (#) g1)) /. clet c be
Element of
C;
( 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))
;
((f / g) (#) (f1 / g1)) /. c = ((f (#) f1) / (g (#) g1)) /. cthen
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
;
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; verum