theorem :: FINSEQ_3:146

for x, y being object
for f1, f2 being Function st x in dom f1 & y in dom f2 holds
for y1, y2 being object holds
( [:f1,f2:] . (x,y) = [y1,y2] iff (Frege <*f1,f2*>) . <*x,y*> = <*y1,y2*> )