per cases ( B = {} or B <> {} ) ;
suppose A1: B = {} ; :: thesis: ex b1 being bifunction of A,B st
( b1 is Covariant & b1 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 b1 being bifunction of A,B st
( b1 is Covariant & b1 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;