let f1, f, g1, g be complex-valued Function; (f1 / f) + (g1 / g) = ((f1 (#) g) + (g1 (#) f)) / (f (#) g)
A1:
now let c be
set ;
( c in dom ((f1 / f) + (g1 / g)) implies ((f1 / f) + (g1 / g)) . c = (((f1 (#) g) + (g1 (#) f)) / (f (#) g)) . c )A2:
dom (g ^ ) c= dom g
by Th11;
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:
dom (f ^ ) c= dom f
by Th11;
A8:
c in (dom (f1 (#) (f ^ ))) /\ (dom (g1 / g))
by A4, Th47;
then
c in dom (f1 (#) (f ^ ))
by XBOOLE_0:def 4;
then A9:
c in (dom f1) /\ (dom (f ^ ))
by VALUED_1:def 4;
then A10:
c in dom (f ^ )
by XBOOLE_0:def 4;
then A11:
f . c <> 0
by Th13;
c in (dom (f1 (#) (f ^ ))) /\ (dom (g1 (#) (g ^ )))
by A8, Th47;
then
c in dom (g1 (#) (g ^ ))
by XBOOLE_0:def 4;
then A12:
c in (dom g1) /\ (dom (g ^ ))
by VALUED_1:def 4;
then A13:
c in dom (g ^ )
by XBOOLE_0:def 4;
then A14:
g . c <> 0
by Th13;
c in dom g1
by A12, XBOOLE_0:def 4;
then
c in (dom g1) /\ (dom f)
by A10, A7, XBOOLE_0:def 4;
then A15:
c in dom (g1 (#) f)
by VALUED_1:def 4;
c in dom f1
by A9, XBOOLE_0:def 4;
then
c in (dom f1) /\ (dom g)
by A13, A2, XBOOLE_0:def 4;
then
c in dom (f1 (#) g)
by VALUED_1:def 4;
then
c in (dom (f1 (#) g)) /\ (dom (g1 (#) f))
by A15, XBOOLE_0:def 4;
then A16:
c in dom ((f1 (#) g) + (g1 (#) f))
by VALUED_1:def 1;
c in (dom (f ^ )) /\ (dom (g ^ ))
by A10, A13, XBOOLE_0:def 4;
then
c in dom ((f ^ ) (#) (g ^ ))
by VALUED_1:def 4;
then
c in dom ((f (#) g) ^ )
by Th43;
then
c in (dom ((f1 (#) g) + (g1 (#) f))) /\ (dom ((f (#) g) ^ ))
by A16, XBOOLE_0:def 4;
then
c in dom (((f1 (#) g) + (g1 (#) f)) (#) ((f (#) g) ^ ))
by VALUED_1:def 4;
then A17:
c in dom (((f1 (#) g) + (g1 (#) f)) / (f (#) g))
by Th47;
thus ((f1 / f) + (g1 / g)) . c =
((f1 / f) . c) + ((g1 / g) . c)
by A3, VALUED_1:def 1
.=
((f1 . c) * ((f . c) " )) + ((g1 / g) . c)
by A5, Def4
.=
((f1 . c) * (1 * ((f . c) " ))) + (((g1 . c) * 1) * ((g . c) " ))
by A6, Def4
.=
((f1 . c) * (((g . c) * ((g . c) " )) * ((f . c) " ))) + ((g1 . c) * (1 * ((g . c) " )))
by A14, XCMPLX_0:def 7
.=
((f1 . c) * ((g . c) * (((g . c) " ) * ((f . c) " )))) + ((g1 . c) * (((f . c) * ((f . c) " )) * ((g . c) " )))
by A11, 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 VALUED_1:5
.=
(((f1 . c) * (g . c)) * (((f (#) g) . c) " )) + ((g1 . c) * ((f . c) * (((f (#) g) . c) " )))
by VALUED_1:5
.=
(((f1 (#) g) . c) * (((f (#) g) . c) " )) + (((g1 . c) * (f . c)) * (((f (#) g) . c) " ))
by VALUED_1:5
.=
(((f1 (#) g) . c) * (((f (#) g) . c) " )) + (((g1 (#) f) . c) * (((f (#) g) . c) " ))
by VALUED_1:5
.=
(((f1 (#) g) . c) + ((g1 (#) f) . c)) * (((f (#) g) . c) " )
.=
(((f1 (#) g) + (g1 (#) f)) . c) * (((f (#) g) . c) " )
by A16, VALUED_1:def 1
.=
(((f1 (#) g) + (g1 (#) f)) / (f (#) g)) . c
by A17, Def4
;
verum end;
dom ((f1 / f) + (g1 / g)) =
(dom (f1 / f)) /\ (dom (g1 / g))
by VALUED_1:def 1
.=
((dom f1) /\ ((dom f) \ (f " {0 }))) /\ (dom (g1 / g))
by Def4
.=
((dom f1) /\ ((dom f) \ (f " {0 }))) /\ ((dom g1) /\ ((dom g) \ (g " {0 })))
by Def4
.=
((dom f1) /\ ((dom f) /\ ((dom f) \ (f " {0 })))) /\ ((dom g1) /\ ((dom g) \ (g " {0 })))
by Th11
.=
(((dom f) /\ ((dom f) \ (f " {0 }))) /\ (dom f1)) /\ (((dom g) /\ ((dom g) \ (g " {0 }))) /\ (dom g1))
by Th11
.=
((dom f) /\ ((dom f) \ (f " {0 }))) /\ ((dom f1) /\ (((dom g) /\ ((dom g) \ (g " {0 }))) /\ (dom g1)))
by XBOOLE_1:16
.=
((dom f) /\ ((dom f) \ (f " {0 }))) /\ (((dom f1) /\ ((dom g) /\ ((dom g) \ (g " {0 })))) /\ (dom g1))
by XBOOLE_1:16
.=
((dom f) /\ ((dom f) \ (f " {0 }))) /\ ((((dom f1) /\ (dom g)) /\ ((dom g) \ (g " {0 }))) /\ (dom g1))
by XBOOLE_1:16
.=
((dom f) /\ ((dom f) \ (f " {0 }))) /\ (((dom (f1 (#) g)) /\ ((dom g) \ (g " {0 }))) /\ (dom g1))
by VALUED_1:def 4
.=
((dom f) /\ ((dom f) \ (f " {0 }))) /\ ((dom (f1 (#) g)) /\ ((dom g1) /\ ((dom g) \ (g " {0 }))))
by XBOOLE_1:16
.=
(dom (f1 (#) g)) /\ ((((dom f) \ (f " {0 })) /\ (dom f)) /\ ((dom g1) /\ ((dom g) \ (g " {0 }))))
by XBOOLE_1:16
.=
(dom (f1 (#) g)) /\ (((dom f) \ (f " {0 })) /\ ((dom f) /\ ((dom g1) /\ ((dom g) \ (g " {0 })))))
by XBOOLE_1:16
.=
(dom (f1 (#) g)) /\ (((dom f) \ (f " {0 })) /\ (((dom g1) /\ (dom f)) /\ ((dom g) \ (g " {0 }))))
by XBOOLE_1:16
.=
(dom (f1 (#) g)) /\ (((dom f) \ (f " {0 })) /\ ((dom (g1 (#) f)) /\ ((dom g) \ (g " {0 }))))
by VALUED_1:def 4
.=
(dom (f1 (#) g)) /\ ((dom (g1 (#) f)) /\ (((dom f) \ (f " {0 })) /\ ((dom g) \ (g " {0 }))))
by XBOOLE_1:16
.=
((dom (f1 (#) g)) /\ (dom (g1 (#) f))) /\ (((dom f) \ (f " {0 })) /\ ((dom g) \ (g " {0 })))
by XBOOLE_1:16
.=
(dom ((f1 (#) g) + (g1 (#) f))) /\ (((dom f) \ (f " {0 })) /\ ((dom g) \ (g " {0 })))
by VALUED_1:def 1
.=
(dom ((f1 (#) g) + (g1 (#) f))) /\ ((dom (f (#) g)) \ ((f (#) g) " {0 }))
by Th12
.=
dom (((f1 (#) g) + (g1 (#) f)) / (f (#) g))
by Def4
;
hence
(f1 / f) + (g1 / g) = ((f1 (#) g) + (g1 (#) f)) / (f (#) g)
by A1, FUNCT_1:9; verum