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_{1} being object holds

( not b_{1} in dom ((g - c1) - c2) or ((g - c1) - c2) . b_{1} = (g - (c1 + c2)) . b_{1} )

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

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

( not 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