let A be set ; :: thesis: for B being non empty set
for b being Element of B
for f being bifunction of A,B st f = [:A,A:] --> [b,b] holds
( f is Covariant & f is Contravariant )
let B be non empty set ; :: thesis: for b being Element of B
for f being bifunction of A,B st f = [:A,A:] --> [b,b] holds
( f is Covariant & f is Contravariant )
let b be Element of B; :: thesis: for f being bifunction of A,B st f = [:A,A:] --> [b,b] holds
( f is Covariant & f is Contravariant )
let f be bifunction of A,B; :: thesis: ( f = [:A,A:] --> [b,b] implies ( f is Covariant & f is Contravariant ) )
assume A1: f = [:A,A:] --> [b,b] ; :: thesis: ( f is Covariant & f is Contravariant )
reconsider g = A --> b as Function of A,B ;
thus f is Covariant :: thesis: f is Contravariant

proof

take g ; :: according to FUNCTOR0:def 1 :: thesis: f = [:g,g:]
thus f = [:g,g:] by A1, ALTCAT_2:1; :: thesis: verum

end;

take g ; :: according to FUNCTOR0:def 2 :: thesis: f = ~ [:g,g:]
[:A,A:] --> [b,b] = ~ ([:A,A:] --> [b,b]) by Th5;
hence f = ~ [:g,g:] by A1, ALTCAT_2:1; :: thesis: verum