let C be non empty set ; for f, f1, g, g1 being PartFunc of C,COMPLEX holds (f1 / f) + (g1 / g) = ((f1 (#) g) + (g1 (#) f)) / (f (#) g)
let f, f1, g, g1 be PartFunc of C,COMPLEX; (f1 / f) + (g1 / g) = ((f1 (#) g) + (g1 (#) f)) / (f (#) g)
A1:
now for c being Element of C st c in dom ((f1 / f) + (g1 / g)) holds
((f1 / f) + (g1 / g)) /. c = (((f1 (#) g) + (g1 (#) f)) / (f (#) g)) /. clet c be
Element of
C;
( c in dom ((f1 / f) + (g1 / g)) implies ((f1 / f) + (g1 / g)) /. c = (((f1 (#) g) + (g1 (#) f)) / (f (#) g)) /. c )A2:
dom (f ^) c= dom f
by Th6;
assume A3:
c in dom ((f1 / f) + (g1 / g))
;
((f1 / f) + (g1 / g)) /. c = (((f1 (#) g) + (g1 (#) f)) / (f (#) g)) /. cthen A4:
c in (dom (f1 / f)) /\ (dom (g1 / g))
by VALUED_1:def 1;
then A5:
c in dom (f1 / f)
by XBOOLE_0:def 4;
A6:
c in dom (g1 / g)
by A4, XBOOLE_0:def 4;
A7:
c in (dom (f1 (#) (f ^))) /\ (dom (g1 / g))
by A4, Th38;
then
c in dom (f1 (#) (f ^))
by XBOOLE_0:def 4;
then A8:
c in (dom f1) /\ (dom (f ^))
by Th3;
then A9:
c in dom (f ^)
by XBOOLE_0:def 4;
then A10:
f /. c <> 0c
by Th8;
c in (dom (f1 (#) (f ^))) /\ (dom (g1 (#) (g ^)))
by A7, Th38;
then
c in dom (g1 (#) (g ^))
by XBOOLE_0:def 4;
then A11:
c in (dom g1) /\ (dom (g ^))
by Th3;
then A12:
c in dom (g ^)
by XBOOLE_0:def 4;
then A13:
g /. c <> 0c
by Th8;
c in dom g1
by A11, XBOOLE_0:def 4;
then
c in (dom g1) /\ (dom f)
by A9, A2, XBOOLE_0:def 4;
then A14:
c in dom (g1 (#) f)
by Th3;
A15:
dom (g ^) c= dom g
by Th6;
then
c in (dom f) /\ (dom g)
by A9, A12, A2, XBOOLE_0:def 4;
then A16:
c in dom (f (#) g)
by Th3;
c in dom f1
by A8, XBOOLE_0:def 4;
then
c in (dom f1) /\ (dom g)
by A12, A15, XBOOLE_0:def 4;
then A17:
c in dom (f1 (#) g)
by Th3;
then
c in (dom (f1 (#) g)) /\ (dom (g1 (#) f))
by A14, XBOOLE_0:def 4;
then A18:
c in dom ((f1 (#) g) + (g1 (#) f))
by VALUED_1:def 1;
c in (dom (f ^)) /\ (dom (g ^))
by A9, A12, XBOOLE_0:def 4;
then
c in dom ((f ^) (#) (g ^))
by Th3;
then
c in dom ((f (#) g) ^)
by Th34;
then
c in (dom ((f1 (#) g) + (g1 (#) f))) /\ (dom ((f (#) g) ^))
by A18, XBOOLE_0:def 4;
then
c in dom (((f1 (#) g) + (g1 (#) f)) (#) ((f (#) g) ^))
by Th3;
then A19:
c in dom (((f1 (#) g) + (g1 (#) f)) / (f (#) g))
by Th38;
thus ((f1 / f) + (g1 / g)) /. c =
((f1 / f) /. c) + ((g1 / g) /. c)
by A3, Th1
.=
((f1 /. c) * ((f /. c) ")) + ((g1 / g) /. c)
by A5, Def1
.=
((f1 /. c) * (1r * ((f /. c) "))) + (((g1 /. c) * 1r) * ((g /. c) "))
by A6, Def1, COMPLEX1:def 4
.=
((f1 /. c) * (((g /. c) * ((g /. c) ")) * ((f /. c) "))) + ((g1 /. c) * (1r * ((g /. c) ")))
by A13, COMPLEX1:def 4, XCMPLX_0:def 7
.=
((f1 /. c) * ((g /. c) * (((g /. c) ") * ((f /. c) ")))) + ((g1 /. c) * (((f /. c) * ((f /. c) ")) * ((g /. c) ")))
by A10, COMPLEX1:def 4, XCMPLX_0:def 7
.=
((f1 /. c) * ((g /. c) * (((g /. c) * (f /. c)) "))) + ((g1 /. c) * ((f /. c) * (((f /. c) ") * ((g /. c) "))))
by XCMPLX_1:204
.=
((f1 /. c) * ((g /. c) * (((f /. c) * (g /. c)) "))) + ((g1 /. c) * ((f /. c) * (((f /. c) * (g /. c)) ")))
by XCMPLX_1:204
.=
((f1 /. c) * ((g /. c) * (((f (#) g) /. c) "))) + ((g1 /. c) * ((f /. c) * (((f /. c) * (g /. c)) ")))
by A16, Th3
.=
(((f1 /. c) * (g /. c)) * (((f (#) g) /. c) ")) + ((g1 /. c) * ((f /. c) * (((f (#) g) /. c) ")))
by A16, Th3
.=
(((f1 (#) g) /. c) * (((f (#) g) /. c) ")) + (((g1 /. c) * (f /. c)) * (((f (#) g) /. c) "))
by A17, Th3
.=
(((f1 (#) g) /. c) * (((f (#) g) /. c) ")) + (((g1 (#) f) /. c) * (((f (#) g) /. c) "))
by A14, Th3
.=
(((f1 (#) g) /. c) + ((g1 (#) f) /. c)) * (((f (#) g) /. c) ")
.=
(((f1 (#) g) + (g1 (#) f)) /. c) * (((f (#) g) /. c) ")
by A18, Th1
.=
(((f1 (#) g) + (g1 (#) f)) / (f (#) g)) /. c
by A19, Def1
;
verum end;
dom ((f1 / f) + (g1 / g)) =
(dom (f1 / f)) /\ (dom (g1 / g))
by VALUED_1:def 1
.=
((dom f1) /\ ((dom f) \ (f " {0c}))) /\ (dom (g1 / g))
by Def1
.=
((dom f1) /\ ((dom f) \ (f " {0c}))) /\ ((dom g1) /\ ((dom g) \ (g " {0c})))
by Def1
.=
((dom f1) /\ ((dom f) /\ ((dom f) \ (f " {0c})))) /\ ((dom g1) /\ ((dom g) \ (g " {0c})))
by Th6
.=
(((dom f) /\ ((dom f) \ (f " {0c}))) /\ (dom f1)) /\ (((dom g) /\ ((dom g) \ (g " {0c}))) /\ (dom g1))
by Th6
.=
((dom f) /\ ((dom f) \ (f " {0c}))) /\ ((dom f1) /\ (((dom g) /\ ((dom g) \ (g " {0c}))) /\ (dom g1)))
by XBOOLE_1:16
.=
((dom f) /\ ((dom f) \ (f " {0c}))) /\ (((dom f1) /\ ((dom g) /\ ((dom g) \ (g " {0c})))) /\ (dom g1))
by XBOOLE_1:16
.=
((dom f) /\ ((dom f) \ (f " {0c}))) /\ ((((dom f1) /\ (dom g)) /\ ((dom g) \ (g " {0c}))) /\ (dom g1))
by XBOOLE_1:16
.=
((dom f) /\ ((dom f) \ (f " {0c}))) /\ (((dom (f1 (#) g)) /\ ((dom g) \ (g " {0c}))) /\ (dom g1))
by Th3
.=
((dom f) /\ ((dom f) \ (f " {0c}))) /\ ((dom (f1 (#) g)) /\ ((dom g1) /\ ((dom g) \ (g " {0c}))))
by XBOOLE_1:16
.=
(dom (f1 (#) g)) /\ ((((dom f) \ (f " {0c})) /\ (dom f)) /\ ((dom g1) /\ ((dom g) \ (g " {0c}))))
by XBOOLE_1:16
.=
(dom (f1 (#) g)) /\ (((dom f) \ (f " {0c})) /\ ((dom f) /\ ((dom g1) /\ ((dom g) \ (g " {0c})))))
by XBOOLE_1:16
.=
(dom (f1 (#) g)) /\ (((dom f) \ (f " {0c})) /\ (((dom g1) /\ (dom f)) /\ ((dom g) \ (g " {0c}))))
by XBOOLE_1:16
.=
(dom (f1 (#) g)) /\ (((dom f) \ (f " {0c})) /\ ((dom (g1 (#) f)) /\ ((dom g) \ (g " {0c}))))
by Th3
.=
(dom (f1 (#) g)) /\ ((dom (g1 (#) f)) /\ (((dom f) \ (f " {0c})) /\ ((dom g) \ (g " {0c}))))
by XBOOLE_1:16
.=
((dom (f1 (#) g)) /\ (dom (g1 (#) f))) /\ (((dom f) \ (f " {0c})) /\ ((dom g) \ (g " {0c})))
by XBOOLE_1:16
.=
(dom ((f1 (#) g) + (g1 (#) f))) /\ (((dom f) \ (f " {0c})) /\ ((dom g) \ (g " {0c})))
by VALUED_1:def 1
.=
(dom ((f1 (#) g) + (g1 (#) f))) /\ ((dom (f (#) g)) \ ((f (#) g) " {0c}))
by Th7
.=
dom (((f1 (#) g) + (g1 (#) f)) / (f (#) g))
by Def1
;
hence
(f1 / f) + (g1 / g) = ((f1 (#) g) + (g1 (#) f)) / (f (#) g)
by A1, PARTFUN2:1; verum