theorem :: FINSEQ_3:140

for x being object
for f, g, h being Function st x in dom h holds
<*f,g,h*> .. (3,x) = h . x