assume a0: ( x = y & a = b ) ; :: thesis: a * x = b * y
c2: ( dom (a * x) = A & dom x = A ) by FUNCT_2:169;
then for c being set st c in dom (a * x) holds
(a * x) . c = b * (y . c) by a0, FUNCSDOM:15;
hence a * x = b * y by a0, c2, VALUED_1:def 5; :: thesis: verum