let c1, c2 be Complex; :: thesis: for g being complex-valued Function holds (g + c1) - c2 = g + (c1 - c2)
let g be complex-valued Function; :: thesis: (g + c1) - c2 = g + (c1 - c2)
A1: dom ((g + c1) - c2) = dom (g + c1) by VALUED_1:def 2;
A2: dom (g + c1) = dom g by VALUED_1:def 2;
hence dom ((g + c1) - c2) = dom (g + (c1 - c2)) by A1, VALUED_1:def 2; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom ((g + c1) - c2) or ((g + c1) - c2) . b₁ = (g + (c1 - c2)) . b₁ )
let x be object ; :: thesis: ( not x in dom ((g + c1) - c2) or ((g + c1) - c2) . x = (g + (c1 - c2)) . x )
A3: dom (g + (c1 - c2)) = dom g by VALUED_1:def 2;
assume A4: x in dom ((g + c1) - c2) ; :: thesis: ((g + c1) - c2) . x = (g + (c1 - c2)) . x
hence ((g + c1) - c2) . x = ((g + c1) . x) - c2 by VALUED_1:def 2
.= ((g . x) + c1) - c2 by A1, A4, VALUED_1:def 2
.= (g . x) + (c1 - c2)
.= (g + (c1 - c2)) . x by A1, A2, A3, A4, VALUED_1:def 2 ;
:: thesis: verum