let x be object ; :: thesis: for X being set
for Y being complex-functions-membered set
for f being PartFunc of X,Y
for g being complex-valued Function st x in dom (f </> g) holds
(f </> g) . x = (f . x) (/) (g . x)
let X be set ; :: thesis: for Y being complex-functions-membered set
for f being PartFunc of X,Y
for g being complex-valued Function st x in dom (f </> g) holds
(f </> g) . x = (f . x) (/) (g . x)
let Y be complex-functions-membered set ; :: thesis: for f being PartFunc of X,Y
for g being complex-valued Function st x in dom (f </> g) holds
(f </> g) . x = (f . x) (/) (g . x)
let f be PartFunc of X,Y; :: thesis: for g being complex-valued Function st x in dom (f </> g) holds
(f </> g) . x = (f . x) (/) (g . x)
let g be complex-valued Function; :: thesis: ( x in dom (f </> g) implies (f </> g) . x = (f . x) (/) (g . x) )
assume x in dom (f </> g) ; :: thesis: (f </> g) . x = (f . x) (/) (g . x)
hence (f </> g) . x = (f . x) (#) ((g ") . x) by Def43
.= (f . x) (/) (g . x) by VALUED_1:10 ;
:: thesis: verum