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:90;
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 1 :: thesis: f = [:g,g:]
thus f = [:h,h:]
.= [:g,g:] ; :: thesis: verum

end;

take g ; :: according to FUNCTOR0:def 2 :: 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 )

set b = the Element of B;
set f = [:A,A:] --> [ the Element of B, the Element of B];
[ the Element of B, the Element of B] in [:B,B:] by A2, ZFMISC_1:87;
then reconsider f = [:A,A:] --> [ the Element of B, the Element of B] as bifunction of A,B by FUNCOP_1:45;
take f ; :: thesis: ( f is Covariant & f is Contravariant )
thus ( f is Covariant & f is Contravariant ) by A2, Th15; :: thesis: verum

end;

end;