let f, g be complex-valued Function; :: thesis: f / g = f (#) (g ^)

A1: now :: thesis: for c being object st c in dom (f / g) holds
(f / g) . c = (f (#) (g ^)) . c

let c be object ; :: thesis: ( c in dom (f / g) implies (f / g) . c = (f (#) (g ^)) . c )
assume A2: c in dom (f / g) ; :: thesis: (f / g) . c = (f (#) (g ^)) . c
then c in (dom f) /\ ((dom g) \ (g " {0})) by Def1;
then c in (dom f) /\ (dom (g ^)) by Def2;
then A3: c in dom (g ^) by XBOOLE_0:def 4;
thus (f / g) . c = (f . c) * ((g . c) ") by A2, Def1
.= (f . c) * ((g ^) . c) by A3, Def2
.= (f (#) (g ^)) . c by VALUED_1:5 ; :: thesis: verum

end;

dom (f / g) = (dom f) /\ ((dom g) \ (g " {0})) by Def1
.= (dom f) /\ (dom (g ^)) by Def2
.= dom (f (#) (g ^)) by VALUED_1:def 4 ;
hence f / g = f (#) (g ^) by A1, FUNCT_1:2; :: thesis: verum