theorem :: FINSEQ_3:139

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