let x be object ; :: according to VALUED_0:def 7 :: thesis: ( not x in dom (f1 / f2) or (f1 / f2) . x is complex )
set F = f1 / f2;
assume x in dom (f1 / f2) ; :: thesis: (f1 / f2) . x is complex
then (f1 / f2) . x = (f1 . x) * ((f2 . x) ") by Def1;
hence (f1 / f2) . x is complex ; :: thesis: verum