let f, f1, g, g1 be complex-valued Function; :: thesis: (f / g) (#) (f1 / g1) = (f (#) f1) / (g (#) g1)
A1: now :: thesis: for c being object st c in dom ((f / g) (#) (f1 / g1)) holds
((f / g) (#) (f1 / g1)) . c = ((f (#) f1) / (g (#) g1)) . c
let c be object ; :: thesis: ( c in dom ((f / g) (#) (f1 / g1)) implies ((f / g) (#) (f1 / g1)) . c = ((f (#) f1) / (g (#) g1)) . c )
assume c in dom ((f / g) (#) (f1 / g1)) ; :: thesis: ((f / g) (#) (f1 / g1)) . c = ((f (#) f1) / (g (#) g1)) . c
thus ((f / g) (#) (f1 / g1)) . c = ((f / g) . c) * ((f1 / g1) . c) by VALUED_1:5
.= ((f (#) (g ^)) . c) * ((f1 / g1) . c) by Th31
.= ((f (#) (g ^)) . c) * ((f1 (#) (g1 ^)) . c) by Th31
.= ((f . c) * ((g ^) . c)) * ((f1 (#) (g1 ^)) . c) by VALUED_1:5
.= ((f . c) * ((g ^) . c)) * ((f1 . c) * ((g1 ^) . c)) by VALUED_1:5
.= (f . c) * ((f1 . c) * (((g ^) . c) * ((g1 ^) . c)))
.= (f . c) * ((f1 . c) * (((g ^) (#) (g1 ^)) . c)) by VALUED_1:5
.= ((f . c) * (f1 . c)) * (((g ^) (#) (g1 ^)) . c)
.= ((f . c) * (f1 . c)) * (((g (#) g1) ^) . c) by Th27
.= ((f (#) f1) . c) * (((g (#) g1) ^) . c) by VALUED_1:5
.= ((f (#) f1) (#) ((g (#) g1) ^)) . c by VALUED_1:5
.= ((f (#) f1) / (g (#) g1)) . c by Th31 ; :: thesis: verum
end;
dom ((f / g) (#) (f1 / g1)) = (dom (f / g)) /\ (dom (f1 / g1)) by VALUED_1:def 4
.= ((dom f) /\ ((dom g) \ (g " ))) /\ (dom (f1 / g1)) by Def1
.= ((dom f) /\ ((dom g) \ (g " ))) /\ ((dom f1) /\ ((dom g1) \ (g1 " ))) by Def1
.= (dom f) /\ (((dom g) \ (g " )) /\ ((dom f1) /\ ((dom g1) \ (g1 " )))) by XBOOLE_1:16
.= (dom f) /\ ((dom f1) /\ (((dom g) \ (g " )) /\ ((dom g1) \ (g1 " )))) by XBOOLE_1:16
.= ((dom f) /\ (dom f1)) /\ (((dom g) \ (g " )) /\ ((dom g1) \ (g1 " ))) by XBOOLE_1:16
.= (dom (f (#) f1)) /\ (((dom g) \ (g " )) /\ ((dom g1) \ (g1 " ))) by VALUED_1:def 4
.= (dom (f (#) f1)) /\ ((dom (g (#) g1)) \ ((g (#) g1) " )) by Th2
.= dom ((f (#) f1) / (g (#) g1)) by Def1 ;
hence (f / g) (#) (f1 / g1) = (f (#) f1) / (g (#) g1) by ; :: thesis: verum