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 Covariant holds
F " is Covariant
let F be feasible FunctorStr of A,B; :: thesis: ( F is bijective & F is Covariant implies F " is Covariant )
assume A1: ( F is bijective & F is Covariant ) ; :: thesis: F " is Covariant
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 Covariant by A1, Def13;
then consider f being Function of the carrier of A, the carrier of B such that
A4: the ObjectMap of F = [:f,f:] by Def2;
A5: f is one-to-one by A2, A4, Th8;
then A6: dom (f ") = rng f by FUNCT_1:33;
A7: rng (f ") = dom f by A5, FUNCT_1:33;
A8: rng [:f,f:] = [: the carrier of B, the carrier of B:] by A3, A4, FUNCT_2:def 3;
rng [:f,f:] = [:(rng f),(rng f):] by FUNCT_3:67;
then rng f = the carrier of B by A8, ZFMISC_1:92;
then reconsider g = f " as Function of the carrier of B, the carrier of A by A6, A7, FUNCT_2:def 1, RELSET_1:4;
take g ; :: according to FUNCTOR0:def 1,FUNCTOR0:def 12 :: thesis: the ObjectMap of (F ") = [:g,g:]
[:f,f:] " = [:g,g:] by A5, Th7;
hence the ObjectMap of (F ") = [:g,g:] by A1, A4, Def39; :: thesis: verum