theorem :: FINSEQ_2:126

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