let X, X1 be set ; :: thesis: for Y, Y1 being complex-functions-membered set
for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1
for g being complex-valued Function st f1 = <-> f holds
f <#> (- g) = f1 <#> g
let Y, Y1 be complex-functions-membered set ; :: thesis: for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1
for g being complex-valued Function st f1 = <-> f holds
f <#> (- g) = f1 <#> g
let f be PartFunc of X,Y; :: thesis: for f1 being PartFunc of X1,Y1
for g being complex-valued Function st f1 = <-> f holds
f <#> (- g) = f1 <#> g
let f1 be PartFunc of X1,Y1; :: thesis: for g being complex-valued Function st f1 = <-> f holds
f <#> (- g) = f1 <#> g
let g be complex-valued Function; :: thesis: ( f1 = <-> f implies f <#> (- g) = f1 <#> g )
assume A1: f1 = <-> f ; :: thesis: f <#> (- g) = f1 <#> g
then A2: dom f1 = dom f by Def32;
A3: dom (f1 <#> g) = (dom f1) /\ (dom g) by Def42;
A9: dom (f <#> (- g)) = (dom f) /\ (dom (- g)) by Def42;
hence A5: dom (f <#> (- g)) = dom (f1 <#> g) by A2, A3, VALUED_1:8; :: according to FUNCT_1:def 17 :: thesis: for b₁ being set holds
( not b₁ in dom (f <#> (- g)) or (f <#> (- g)) . b₁ = (f1 <#> g) . b₁ )
let x be set ; :: thesis: ( not x in dom (f <#> (- g)) or (f <#> (- g)) . x = (f1 <#> g) . x )
assume A6: x in dom (f <#> (- g)) ; :: thesis: (f <#> (- g)) . x = (f1 <#> g) . x
then A7: x in dom f1 by A9, A2, XBOOLE_0:def 4;
thus (f <#> (- g)) . x = (f . x) (#) ((- g) . x) by A6, Def42
.= (f . x) (#) (- (g . x)) by VALUED_1:8
.= (- (f . x)) (#) (g . x) by Th17
.= (f1 . x) (#) (g . x) by A1, A7, Def32
.= (f1 <#> g) . x by A6, A5, Def42 ; :: thesis: verum