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

.= (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

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

(f / g) . c = (f (#) (g ^)) . c

dom (f / g) =
(dom f) /\ ((dom g) \ (g " {0}))
by Def1
(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;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

.= (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