:: deftheorem Def2 defines Contravariant FUNCTOR0:def 2 :
for A, B being set
for f being bifunction of A,B holds
( f is Contravariant iff ex g being Function of A,B st f = ~ [:g,g:] );