theorem :: FUNCTOR0:16

for A, B being non empty set
for f being Covariant Contravariant bifunction of A,B ex b being Element of B st f = [:A,A:] --> [b,b]