let A, B be non empty transitive with_units AltCatStr ; :: thesis: for F being reflexive feasible FunctorStr of A,B st F is bijective & F is coreflexive & F is Covariant holds
for o1, o2 being object of B
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(Morph-Map F,((F " ) . o1),((F " ) . o2)) . ((Morph-Map (F " ),o1,o2) . m) = m
let F be reflexive feasible FunctorStr of A,B; :: thesis: ( F is bijective & F is coreflexive & F is Covariant implies for o1, o2 being object of B
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(Morph-Map F,((F " ) . o1),((F " ) . o2)) . ((Morph-Map (F " ),o1,o2) . m) = m )
assume A1: ( F is bijective & F is coreflexive & F is Covariant ) ; :: thesis: for o1, o2 being object of B
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(Morph-Map F,((F " ) . o1),((F " ) . o2)) . ((Morph-Map (F " ),o1,o2) . m) = m
set G = F " ;
A2: F " is Covariant by A1, Th39;
reconsider H = F " as reflexive feasible FunctorStr of B,A by A1, Th36, Th37;
A3: the ObjectMap of (F " ) = the ObjectMap of F " by A1, Def39;
consider f being ManySortedFunction of the Arrows of A,the Arrows of B * the ObjectMap of F such that
A4: f = the MorphMap of F and
A5: the MorphMap of (F " ) = (f "" ) * (the ObjectMap of F " ) by A1, Def39;
F is injective by A1, Def36;
then F is faithful by Def34;
then A6: the MorphMap of F is "1-1" by Def31;
F is surjective by A1, Def36;
then F is full by Def35;
then A7: ex f being ManySortedFunction of the Arrows of A,the Arrows of B * the ObjectMap of F st
( f = the MorphMap of F & f is "onto" ) by Def33;
let o1, o2 be object of B; :: thesis: for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(Morph-Map F,((F " ) . o1),((F " ) . o2)) . ((Morph-Map (F " ),o1,o2) . m) = m
let m be Morphism of o1,o2; :: thesis: ( <^o1,o2^> <> {} implies (Morph-Map F,((F " ) . o1),((F " ) . o2)) . ((Morph-Map (F " ),o1,o2) . m) = m )
assume A8: <^o1,o2^> <> {} ; :: thesis: (Morph-Map F,((F " ) . o1),((F " ) . o2)) . ((Morph-Map (F " ),o1,o2) . m) = m
A9: [((F " ) . o1),((F " ) . o2)] in [:the carrier of A,the carrier of A:] by ZFMISC_1:106;
A10: [o1,o2] in [:the carrier of B,the carrier of B:] by ZFMISC_1:106;
then A11: [o1,o2] in dom the ObjectMap of (F " ) by FUNCT_2:def 1;
dom the MorphMap of F = [:the carrier of A,the carrier of A:] by PARTFUN1:def 4;
then [((F " ) . o1),((F " ) . o2)] in dom the MorphMap of F by ZFMISC_1:106;
then A12: Morph-Map F,((F " ) . o1),((F " ) . o2) is one-to-one by A6, MSUALG_3:def 2;
(the Arrows of A * the ObjectMap of (F " )) . [o1,o2] = the Arrows of A . (the ObjectMap of H . o1,o2) by A11, FUNCT_1:23
.= the Arrows of A . (H . o1),(H . o2) by A2, Th23
.= <^(H . o1),(H . o2)^> by ALTCAT_1:def 2 ;
then A13: (the Arrows of A * the ObjectMap of (F " )) . [o1,o2] <> {} by A2, A8, Def19;
the MorphMap of (F " ) is ManySortedFunction of the Arrows of B,the Arrows of A * the ObjectMap of (F " ) by Def5;
then Morph-Map (F " ),o1,o2 is Function of (the Arrows of B . [o1,o2]),((the Arrows of A * the ObjectMap of (F " )) . [o1,o2]) by A10, PBOOLE:def 18;
then A14: dom (Morph-Map (F " ),o1,o2) = the Arrows of B . o1,o2 by A13, FUNCT_2:def 1
.= <^o1,o2^> by ALTCAT_1:def 2 ;
A15: Morph-Map (F " ),o1,o2 = (f "" ) . (the ObjectMap of (F " ) . o1,o2) by A3, A5, A11, FUNCT_1:23
.= (f "" ) . [(H . o1),(H . o2)] by A2, Th23
.= (Morph-Map F,((F " ) . o1),((F " ) . o2)) " by A4, A6, A7, A9, MSUALG_3:def 5 ;
thus (Morph-Map F,((F " ) . o1),((F " ) . o2)) . ((Morph-Map (F " ),o1,o2) . m) = ((Morph-Map F,((F " ) . o1),((F " ) . o2)) * (Morph-Map (F " ),o1,o2)) . m by A8, A14, FUNCT_1:23
.= (id (rng (Morph-Map F,((F " ) . o1),((F " ) . o2)))) . m by A12, A15, FUNCT_1:61
.= (id (dom (Morph-Map (F " ),o1,o2))) . m by A12, A15, FUNCT_1:55
.= m by A8, A14, FUNCT_1:35 ; :: thesis: verum