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 " {0}))) /\ (dom (f1 / g1)) by Def1
.= ((dom f) /\ ((dom g) \ (g " {0}))) /\ ((dom f1) /\ ((dom g1) \ (g1 " {0}))) by Def1
.= (dom f) /\ (((dom g) \ (g " {0})) /\ ((dom f1) /\ ((dom g1) \ (g1 " {0})))) by XBOOLE_1:16
.= (dom f) /\ ((dom f1) /\ (((dom g) \ (g " {0})) /\ ((dom g1) \ (g1 " {0})))) by XBOOLE_1:16
.= ((dom f) /\ (dom f1)) /\ (((dom g) \ (g " {0})) /\ ((dom g1) \ (g1 " {0}))) by XBOOLE_1:16
.= (dom (f (#) f1)) /\ (((dom g) \ (g " {0})) /\ ((dom g1) \ (g1 " {0}))) by VALUED_1:def 4
.= (dom (f (#) f1)) /\ ((dom (g (#) g1)) \ ((g (#) g1) " {0})) by Th2
.= dom ((f (#) f1) / (g (#) g1)) by Def1 ;
hence (f / g) (#) (f1 / g1) = (f (#) f1) / (g (#) g1) by A1, FUNCT_1:2; :: thesis: verum