f . [x,y] is Element of (RealPoset [.0 ,1.]) ;
hence f . x,y is Element of (RealPoset [.0 ,1.]) ; :: thesis: verum