theorem :: FINSEQ_2:125

for f being Function
for x, y being set st x in dom f & y in dom f holds
f * <*x,y*> = <*(f . x),(f . y)*>