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

A1: now

let c be set ; :: 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 Def4;
then c in (dom f) /\ (dom (g ^ )) by Def8;
then A3: c in dom (g ^ ) by XBOOLE_0:def 4;
thus (f / g) . c = (f . c) * ((g . c) " ) by A2, Def4
.= (f . c) * ((g ^ ) . c) by A3, Def8
.= (f (#) (g ^ )) . c by VALUED_1:5 ; :: thesis: verum

end;

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