let C be non empty set ; for f, g being PartFunc of C,COMPLEX holds (f / g) (#) g = f | (dom (g ^))
let f, g be PartFunc of C,COMPLEX; (f / g) (#) g = f | (dom (g ^))
A1: dom ((f / g) (#) g) =
(dom (f / g)) /\ (dom g)
by Th3
.=
((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 Th6, XBOOLE_1:28
.=
dom (f | (dom (g ^)))
by RELAT_1:61
;
now for c being Element of C st c in dom ((f / g) (#) g) holds
((f / g) (#) g) /. c = (f | (dom (g ^))) /. clet c be
Element of
C;
( c in dom ((f / g) (#) g) implies ((f / g) (#) g) /. c = (f | (dom (g ^))) /. c )assume A2:
c in dom ((f / g) (#) g)
;
((f / g) (#) g) /. c = (f | (dom (g ^))) /. cthen A3:
c in (dom f) /\ (dom (g ^))
by A1, RELAT_1:61;
then A4:
c in dom (f (#) (g ^))
by Th3;
A5:
c in dom (g ^)
by A3, XBOOLE_0:def 4;
then A6:
g /. c <> 0c
by Th8;
thus ((f / g) (#) g) /. c =
((f / g) /. c) * (g /. c)
by A2, Th3
.=
((f (#) (g ^)) /. c) * (g /. c)
by Th38
.=
((f /. c) * ((g ^) /. c)) * (g /. c)
by A4, Th3
.=
((f /. c) * ((g /. c) ")) * (g /. c)
by A5, Def2
.=
(f /. c) * (((g /. c) ") * (g /. c))
.=
(f /. c) * 1r
by A6, COMPLEX1:def 4, XCMPLX_0:def 7
.=
(f | (dom (g ^))) /. c
by A1, A2, COMPLEX1:def 4, PARTFUN2:15
;
verum end;
hence
(f / g) (#) g = f | (dom (g ^))
by A1, PARTFUN2:1; verum