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

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