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