let f1, f2 be complex-valued Function; :: thesis: for c being object holds (f1 /" f2) . c = (f1 . c) / (f2 . c)
let c be object ; :: thesis: (f1 /" f2) . c = (f1 . c) / (f2 . c)
A1: dom (f1 /" f2) = (dom f1) /\ (dom f2) by Th16;

per cases ( c in dom (f1 /" f2) or not c in dom (f1 /" f2) ) ;

suppose c in dom (f1 /" f2) ; :: thesis: (f1 /" f2) . c = (f1 . c) / (f2 . c)

hence (f1 /" f2) . c = (f1 . c) * ((f2 ") . c) by Def4
.= (f1 . c) / (f2 . c) by Th10 ;
:: thesis: verum

end;

suppose A2: not c in dom (f1 /" f2) ; :: thesis: (f1 /" f2) . c = (f1 . c) / (f2 . c)

then ( not c in dom f1 or not c in dom f2 ) by A1, XBOOLE_0:def 4;
then A3: ( f1 . c = 0 or f2 . c = 0 ) by FUNCT_1:def 2;
thus (f1 /" f2) . c = 0 / 0 by A2, FUNCT_1:def 2
.= (f1 . c) / (f2 . c) by A3 ; :: thesis: verum

end;

end;