let A, B be non empty transitive with_units AltCatStr ; :: thesis: for F being feasible FunctorStr of A,B st F is bijective & F is Contravariant holds
F " is Contravariant
let F be feasible FunctorStr of A,B; :: thesis: ( F is bijective & F is Contravariant implies F " is Contravariant )
assume A1: ( F is bijective & F is Contravariant ) ; :: thesis: F " is Contravariant
then F is injective by Def36;
then F is one-to-one by Def34;
then A2: the ObjectMap of F is one-to-one by Def7;
F is surjective by A1, Def36;
then F is onto by Def35;
then A3: the ObjectMap of F is onto by Def8;
the ObjectMap of F is Contravariant by A1, Def14;
then consider f being Function of the carrier of A,the carrier of B such that
A4: the ObjectMap of F = ~ [:f,f:] by Def3;
[:f,f:] is one-to-one by A2, A4, Th10;
then A5: f is one-to-one by Th8;
then A6: ( dom (f " ) = rng f & rng (f " ) = dom f ) by FUNCT_1:55;
[:f,f:] is onto by A3, A4, Th14;
then A7: rng [:f,f:] = [:the carrier of B,the carrier of B:] by FUNCT_2:def 3;
rng [:f,f:] = [:(rng f),(rng f):] by FUNCT_3:88;
then rng f = the carrier of B by A7, ZFMISC_1:115;
then reconsider g = f " as Function of the carrier of B,the carrier of A by A6, FUNCT_2:def 1, RELSET_1:11;
take g ; :: according to FUNCTOR0:def 3,FUNCTOR0:def 14 :: thesis: the ObjectMap of (F " ) = ~ [:g,g:]
A8: [:f,f:] " = [:g,g:] by A5, Th7;
thus the ObjectMap of (F " ) = the ObjectMap of F " by A1, Def39
.= ~ [:g,g:] by A4, A5, A8, Th11 ; :: thesis: verum