let C be non empty set ; :: thesis: for f1, f, g1, g being PartFunc of C,COMPLEX holds (f1 / f) + (g1 / g) = ((f1 (#) g) + (g1 (#) f)) / (f (#) g)
let f1, f, g1, g be PartFunc of C,COMPLEX ; :: thesis: (f1 / f) + (g1 / g) = ((f1 (#) g) + (g1 (#) f)) / (f (#) g)
A1: 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 Th15
.=
(((dom f) /\ ((dom f) \ (f " {0c }))) /\ (dom f1)) /\ (((dom g) /\ ((dom g) \ (g " {0c }))) /\ (dom g1))
by Th15
.=
((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 Th5
.=
((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 Th5
.=
(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 Th16
.=
dom (((f1 (#) g) + (g1 (#) f)) / (f (#) g))
by Def1
;
now let c be
Element of
C;
:: thesis: ( c in dom ((f1 / f) + (g1 / g)) implies ((f1 / f) + (g1 / g)) /. c = (((f1 (#) g) + (g1 (#) f)) / (f (#) g)) /. c )assume A2:
c in dom ((f1 / f) + (g1 / g))
;
:: thesis: ((f1 / f) + (g1 / g)) /. c = (((f1 (#) g) + (g1 (#) f)) / (f (#) g)) /. cthen A3:
c in (dom (f1 / f)) /\ (dom (g1 / g))
by VALUED_1:def 1;
then A4:
(
c in dom (f1 / f) &
c in dom (g1 / g) )
by XBOOLE_0:def 4;
c in (dom (f1 (#) (f ^ ))) /\ (dom (g1 / g))
by A3, Th51;
then
c in (dom (f1 (#) (f ^ ))) /\ (dom (g1 (#) (g ^ )))
by Th51;
then
(
c in dom (f1 (#) (f ^ )) &
c in dom (g1 (#) (g ^ )) )
by XBOOLE_0:def 4;
then
(
c in (dom f1) /\ (dom (f ^ )) &
c in (dom g1) /\ (dom (g ^ )) )
by Th5;
then A5:
(
c in dom f1 &
c in dom (f ^ ) &
c in dom g1 &
c in dom (g ^ ) )
by XBOOLE_0:def 4;
then A6:
(
f /. c <> 0c &
g /. c <> 0c )
by Th17;
(
c in (dom f1) /\ (dom g1) &
c in (dom (f ^ )) /\ (dom (g ^ )) )
by A5, XBOOLE_0:def 4;
then
(
c in (dom f1) /\ (dom g1) &
c in dom ((f ^ ) (#) (g ^ )) )
by Th5;
then A7:
(
c in (dom f1) /\ (dom g1) &
c in dom ((f (#) g) ^ ) )
by Th45;
A8:
(
dom (g ^ ) c= dom g &
dom (f ^ ) c= dom f )
by Th15;
then
c in (dom f) /\ (dom g)
by A5, XBOOLE_0:def 4;
then A9:
c in dom (f (#) g)
by Th5;
(
c in (dom f1) /\ (dom g) &
c in (dom g1) /\ (dom f) )
by A5, A8, XBOOLE_0:def 4;
then A10:
(
c in dom (f1 (#) g) &
c in dom (g1 (#) f) )
by Th5;
then
c in (dom (f1 (#) g)) /\ (dom (g1 (#) f))
by XBOOLE_0:def 4;
then A11:
c in dom ((f1 (#) g) + (g1 (#) f))
by VALUED_1:def 1;
then
c in (dom ((f1 (#) g) + (g1 (#) f))) /\ (dom ((f (#) g) ^ ))
by A7, XBOOLE_0:def 4;
then
c in dom (((f1 (#) g) + (g1 (#) f)) (#) ((f (#) g) ^ ))
by Th5;
then A12:
c in dom (((f1 (#) g) + (g1 (#) f)) / (f (#) g))
by Th51;
thus ((f1 / f) + (g1 / g)) /. c =
((f1 / f) /. c) + ((g1 / g) /. c)
by A2, Th3
.=
((f1 /. c) * ((f /. c) " )) + ((g1 / g) /. c)
by A4, Def1
.=
((f1 /. c) * (1r * ((f /. c) " ))) + (((g1 /. c) * 1r ) * ((g /. c) " ))
by A4, Def1, COMPLEX1:def 7
.=
((f1 /. c) * (((g /. c) * ((g /. c) " )) * ((f /. c) " ))) + ((g1 /. c) * (1r * ((g /. c) " )))
by A6, COMPLEX1:def 7, XCMPLX_0:def 7
.=
((f1 /. c) * ((g /. c) * (((g /. c) " ) * ((f /. c) " )))) + ((g1 /. c) * (((f /. c) * ((f /. c) " )) * ((g /. c) " )))
by A6, COMPLEX1:def 7, XCMPLX_0:def 7
.=
((f1 /. c) * ((g /. c) * (((g /. c) * (f /. c)) " ))) + ((g1 /. c) * ((f /. c) * (((f /. c) " ) * ((g /. c) " ))))
by XCMPLX_1:205
.=
((f1 /. c) * ((g /. c) * (((f /. c) * (g /. c)) " ))) + ((g1 /. c) * ((f /. c) * (((f /. c) * (g /. c)) " )))
by XCMPLX_1:205
.=
((f1 /. c) * ((g /. c) * (((f (#) g) /. c) " ))) + ((g1 /. c) * ((f /. c) * (((f /. c) * (g /. c)) " )))
by A9, Th5
.=
(((f1 /. c) * (g /. c)) * (((f (#) g) /. c) " )) + ((g1 /. c) * ((f /. c) * (((f (#) g) /. c) " )))
by A9, Th5
.=
(((f1 (#) g) /. c) * (((f (#) g) /. c) " )) + (((g1 /. c) * (f /. c)) * (((f (#) g) /. c) " ))
by A10, Th5
.=
(((f1 (#) g) /. c) * (((f (#) g) /. c) " )) + (((g1 (#) f) /. c) * (((f (#) g) /. c) " ))
by A10, Th5
.=
(((f1 (#) g) /. c) + ((g1 (#) f) /. c)) * (((f (#) g) /. c) " )
.=
(((f1 (#) g) + (g1 (#) f)) /. c) * (((f (#) g) /. c) " )
by A11, Th3
.=
(((f1 (#) g) + (g1 (#) f)) / (f (#) g)) /. c
by A12, Def1
;
:: thesis: verum end;
hence
(f1 / f) + (g1 / g) = ((f1 (#) g) + (g1 (#) f)) / (f (#) g)
by A1, PARTFUN2:3; :: thesis: verum