consider x, y being object such that
A1: ( x in X & y in Y & f = <*x,y*> ) by FINSEQ_3:124;
thus f . 1 is integer by A1, FINSEQ_1:44; :: thesis: verum