let f, g be complex-valued Function; :: thesis: (f / g) (#) g = f | (dom (g ^))
A1: dom ((f / g) (#) g) = (dom (f / g)) /\ (dom g) by VALUED_1:def 4
.= ((dom f) /\ ((dom g) \ (g " ))) /\ (dom g) by Def1
.= (dom f) /\ (((dom g) \ (g " )) /\ (dom g)) by XBOOLE_1:16
.= (dom f) /\ ((dom (g ^)) /\ (dom g)) by Def2
.= (dom f) /\ (dom (g ^)) by
.= dom (f | (dom (g ^))) by RELAT_1:61 ;
now :: thesis: for c being object st c in dom ((f / g) (#) g) holds
((f / g) (#) g) . c = (f | (dom (g ^))) . c
let c be object ; :: thesis: ( c in dom ((f / g) (#) g) implies ((f / g) (#) g) . c = (f | (dom (g ^))) . c )
assume A2: c in dom ((f / g) (#) g) ; :: thesis: ((f / g) (#) g) . c = (f | (dom (g ^))) . c
then c in (dom f) /\ (dom (g ^)) by ;
then A3: c in dom (g ^) by XBOOLE_0:def 4;
then A4: g . c <> 0 by Th3;
thus ((f / g) (#) g) . c = ((f / g) . c) * (g . c) by VALUED_1:5
.= ((f (#) (g ^)) . c) * (g . c) by Th31
.= ((f . c) * ((g ^) . c)) * (g . c) by VALUED_1:5
.= ((f . c) * ((g . c) ")) * (g . c) by
.= (f . c) * (((g . c) ") * (g . c))
.= (f . c) * 1 by
.= (f | (dom (g ^))) . c by ; :: thesis: verum
end;
hence (f / g) (#) g = f | (dom (g ^)) by ; :: thesis: verum