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 Def41
.= (f . x) - (g . x) by VALUED_1:8 ;
:: thesis: verum