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