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