let f, f1, g, g1 be complex-valued Function; :: thesis: (f1 / f) + (g1 / g) = ((f1 (#) g) + (g1 (#) f)) / (f (#) g)
A1: now :: thesis: for c being object st c in dom ((f1 / f) + (g1 / g)) holds
((f1 / f) + (g1 / g)) . c = (((f1 (#) g) + (g1 (#) f)) / (f (#) g)) . c
let c be object ; :: thesis: ( 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 Th1;
assume A3: c in dom ((f1 / f) + (g1 / g)) ; :: thesis: ((f1 / f) + (g1 / g)) . c = (((f1 (#) g) + (g1 (#) f)) / (f (#) g)) . c
then 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 ;
A7: dom (f ^) c= dom f by Th1;
A8: c in (dom (f1 (#) (f ^))) /\ (dom (g1 / g)) by ;
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 Th3;
c in (dom (f1 (#) (f ^))) /\ (dom (g1 (#) (g ^))) by ;
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 Th3;
c in dom g1 by ;
then c in (dom g1) /\ (dom f) by ;
then A15: c in dom (g1 (#) f) by VALUED_1:def 4;
c in dom f1 by ;
then c in (dom f1) /\ (dom g) by ;
then c in dom (f1 (#) g) by VALUED_1:def 4;
then c in (dom (f1 (#) g)) /\ (dom (g1 (#) f)) by ;
then A16: c in dom ((f1 (#) g) + (g1 (#) f)) by VALUED_1:def 1;
c in (dom (f ^)) /\ (dom (g ^)) by ;
then c in dom ((f ^) (#) (g ^)) by VALUED_1:def 4;
then c in dom ((f (#) g) ^) by Th27;
then c in (dom ((f1 (#) g) + (g1 (#) f))) /\ (dom ((f (#) g) ^)) by ;
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 Th31;
thus ((f1 / f) + (g1 / g)) . c = ((f1 / f) . c) + ((g1 / g) . c) by
.= ((f1 . c) * ((f . c) ")) + ((g1 / g) . c) by
.= ((f1 . c) * (1 * ((f . c) "))) + (((g1 . c) * 1) * ((g . c) ")) by
.= ((f1 . c) * (((g . c) * ((g . c) ")) * ((f . c) "))) + ((g1 . c) * (1 * ((g . c) "))) by
.= ((f1 . c) * ((g . c) * (((g . c) ") * ((f . c) ")))) + ((g1 . c) * (((f . c) * ((f . c) ")) * ((g . c) "))) by
.= ((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 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
.= (((f1 (#) g) + (g1 (#) f)) / (f (#) g)) . c by ; :: thesis: verum
end;
dom ((f1 / f) + (g1 / g)) = (dom (f1 / f)) /\ (dom (g1 / g)) by VALUED_1:def 1
.= ((dom f1) /\ ((dom f) \ (f " ))) /\ (dom (g1 / g)) by Def1
.= ((dom f1) /\ ((dom f) \ (f " ))) /\ ((dom g1) /\ ((dom g) \ (g " ))) by Def1
.= ((dom f1) /\ ((dom f) /\ ((dom f) \ (f " )))) /\ ((dom g1) /\ ((dom g) \ (g " ))) by Th1
.= (((dom f) /\ ((dom f) \ (f " ))) /\ (dom f1)) /\ (((dom g) /\ ((dom g) \ (g " ))) /\ (dom g1)) by Th1
.= ((dom f) /\ ((dom f) \ (f " ))) /\ ((dom f1) /\ (((dom g) /\ ((dom g) \ (g " ))) /\ (dom g1))) by XBOOLE_1:16
.= ((dom f) /\ ((dom f) \ (f " ))) /\ (((dom f1) /\ ((dom g) /\ ((dom g) \ (g " )))) /\ (dom g1)) by XBOOLE_1:16
.= ((dom f) /\ ((dom f) \ (f " ))) /\ ((((dom f1) /\ (dom g)) /\ ((dom g) \ (g " ))) /\ (dom g1)) by XBOOLE_1:16
.= ((dom f) /\ ((dom f) \ (f " ))) /\ (((dom (f1 (#) g)) /\ ((dom g) \ (g " ))) /\ (dom g1)) by VALUED_1:def 4
.= ((dom f) /\ ((dom f) \ (f " ))) /\ ((dom (f1 (#) g)) /\ ((dom g1) /\ ((dom g) \ (g " )))) by XBOOLE_1:16
.= (dom (f1 (#) g)) /\ ((((dom f) \ (f " )) /\ (dom f)) /\ ((dom g1) /\ ((dom g) \ (g " )))) by XBOOLE_1:16
.= (dom (f1 (#) g)) /\ (((dom f) \ (f " )) /\ ((dom f) /\ ((dom g1) /\ ((dom g) \ (g " ))))) by XBOOLE_1:16
.= (dom (f1 (#) g)) /\ (((dom f) \ (f " )) /\ (((dom g1) /\ (dom f)) /\ ((dom g) \ (g " )))) by XBOOLE_1:16
.= (dom (f1 (#) g)) /\ (((dom f) \ (f " )) /\ ((dom (g1 (#) f)) /\ ((dom g) \ (g " )))) by VALUED_1:def 4
.= (dom (f1 (#) g)) /\ ((dom (g1 (#) f)) /\ (((dom f) \ (f " )) /\ ((dom g) \ (g " )))) by XBOOLE_1:16
.= ((dom (f1 (#) g)) /\ (dom (g1 (#) f))) /\ (((dom f) \ (f " )) /\ ((dom g) \ (g " ))) by XBOOLE_1:16
.= (dom ((f1 (#) g) + (g1 (#) f))) /\ (((dom f) \ (f " )) /\ ((dom g) \ (g " ))) by VALUED_1:def 1
.= (dom ((f1 (#) g) + (g1 (#) f))) /\ ((dom (f (#) g)) \ ((f (#) g) " )) by Th2
.= dom (((f1 (#) g) + (g1 (#) f)) / (f (#) g)) by Def1 ;
hence (f1 / f) + (g1 / g) = ((f1 (#) g) + (g1 (#) f)) / (f (#) g) by ; :: thesis: verum