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