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