( 0 <= (@ f) . x & (@ f) . x <= 1 ) by FUZZY_2:1;
hence f . x is Element of (RealPoset [.0 ,1.]) ; :: thesis: verum