f . (s,I) is Element of Funcs (X,INT) ;
hence f . (s,I) is Element of Funcs (X,INT) ; :: thesis: verum