let f be complex-valued Function; :: thesis: for g being Function st dom f = dom g & ( for c being object st c in dom f holds
g . c = - (f . c) ) holds
g = - f
let g be Function; :: thesis: ( dom f = dom g & ( for c being object st c in dom f holds
g . c = - (f . c) ) implies g = - f )
assume that
A1: dom f = dom g and
A2: for c being object st c in dom f holds
g . c = - (f . c) ; :: thesis: g = - f
thus dom (- f) = dom g by A1, Def5; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom g or g . b₁ = (- f) . b₁ )
let c be object ; :: thesis: ( not c in dom g or g . c = (- f) . c )
assume A3: c in dom g ; :: thesis: g . c = (- f) . c
thus (- f) . c = - (f . c) by Th8
.= g . c by A1, A2, A3 ; :: thesis: verum