let f be complex-valued Function; :: thesis: for x1, x2 being Complex holds (f + x1) + x2 = f + (x1 + x2)
let x1, x2 be Complex; :: thesis: (f + x1) + x2 = f + (x1 + x2)
reconsider X = dom f as set ;
A1: ( dom ((f + x1) + x2) = dom (f + x1) & ( for c being object st c in dom ((f + x1) + x2) holds
((f + x1) + x2) . c = ((f + x1) . c) + x2 ) ) by VALUED_1:def 2;
A2: ( dom (f + x1) = dom f & ( for c being object st c in dom (f + x1) holds
(f + x1) . c = (f . c) + x1 ) ) by VALUED_1:def 2;
A3: ( dom (f + (x1 + x2)) = dom f & ( for c being object st c in dom (f + (x1 + x2)) holds
(f + (x1 + x2)) . c = (f . c) + (x1 + x2) ) ) by VALUED_1:def 2;
for c being object st c in X holds
((f + x1) + x2) . c = (f + (x1 + x2)) . c

proof

let c be object ; :: thesis: ( c in X implies ((f + x1) + x2) . c = (f + (x1 + x2)) . c )
assume B1: c in X ; :: thesis: ((f + x1) + x2) . c = (f + (x1 + x2)) . c
((f + x1) + x2) . c = ((f + x1) . c) + x2 by A1, A2, B1
.= ((f . c) + x1) + x2 by A2, B1
.= (f . c) + (x1 + x2)
.= (f + (x1 + x2)) . c by A3, B1 ;
hence ((f + x1) + x2) . c = (f + (x1 + x2)) . c ; :: thesis: verum

end;

hence (f + x1) + x2 = f + (x1 + x2) by A1, A2, A3, FUNCT_1:2; :: thesis: verum