s . (@ t) = s . t ;
hence s . t is Integer ; :: thesis: verum