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