theorem Th53: :: FVSUM_1:53

for i being Nat
for K being non empty multMagma
for a1, a2 being Element of K holds a1 * (i |-> a2) = i |-> (a1 * a2)