assume a0: ( x = a & y = b ) ; :: thesis: x + y = a + b
c2: ( dom (x + y) = A & dom x = A & dom y = A ) by FUNCT_2:169;
then c1: dom (x + y) = (dom a) /\ (dom b) by a0;
for c being set st c in dom (x + y) holds
(x + y) . c = (a . c) + (b . c) by a0, c2, FUNCSDOM:10;
hence x + y = a + b by c1, VALUED_1:def 1; :: thesis: verum