f . r,s = f . [r,s] ;
hence f . r,s is Point of T ; :: thesis: verum