theorem :: FINSEQ_3:145

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