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

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