A1: dom y = A by FUNCT_2:92;
assume that
A2: x = a and
A3: y = b ; :: thesis: x + y = a + b
dom (x + y) = A by FUNCT_2:92;
then A4: for c being object st c in dom (x + y) holds
(x + y) . c = (a . c) + (b . c) by A2, A3, FUNCSDOM:1;
dom x = A by FUNCT_2:92;
then dom (x + y) = (dom a) /\ (dom b) by A2, A3, A1, FUNCT_2:92;
hence x + y = a + b by A4, VALUED_1:def 1; :: thesis: verum