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