F | C = F * (incl C) ;
hence F | C is strict contravariant Functor of C,B ; :: thesis: verum