let A, B be non empty transitive with_units AltCatStr ; :: thesis: ( ex F being Functor of A,B st
( F is bijective & F is contravariant ) implies ex F being Functor of B,A st
( F is bijective & F is contravariant ) )
given F being Functor of A,B such that A3: ( F is bijective & F is contravariant ) ; :: thesis: ex F being Functor of B,A st
( F is bijective & F is contravariant )
consider G being Functor of B,A such that
G = F " and
A4: ( G is bijective & G is contravariant ) by A3, Th49;
take G ; :: thesis: ( G is bijective & G is contravariant )
thus ( G is bijective & G is contravariant ) by A4; :: thesis: verum