per cases ( B = {} or B <> {} ) ;

suppose A1: B = {} ; :: thesis: ex b₁ being bifunction of A,B st
( b₁ is Covariant & b₁ is Contravariant )

then [:B,B:] = {} by ZFMISC_1:113;
then reconsider f = {} as bifunction of A,B by Th1;
take f ; :: thesis: ( f is Covariant & f is Contravariant )
reconsider g = {} as Function of A,B by A1, Th1;
reconsider h = g as empty Function ;
thus f is Covariant :: thesis: f is Contravariant

proof

take g ; :: according to FUNCTOR0:def 2 :: thesis: f = [:g,g:]
thus f = [:h,h:]
.= [:g,g:] ; :: thesis: verum

end;

take g ; :: according to FUNCTOR0:def 3 :: thesis: f = ~ [:g,g:]
thus f = ~ [:h,h:]
.= ~ [:g,g:] ; :: thesis: verum

end;

suppose A2: B <> {} ; :: thesis: ex b₁ being bifunction of A,B st
( b₁ is Covariant & b₁ is Contravariant )

consider b being Element of B;
set f = [:A,A:] --> [b,b];
[b,b] in [:B,B:] by A2, ZFMISC_1:106;
then reconsider f = [:A,A:] --> [b,b] as bifunction of A,B by FUNCOP_1:57;
take f ; :: thesis: ( f is Covariant & f is Contravariant )
thus ( f is Covariant & f is Contravariant ) by A2, Th16; :: thesis: verum

end;

end;