let A, B be non empty transitive with_units AltCatStr ; for F being reflexive feasible FunctorStr of A,B st F is bijective & F is coreflexive & F is Contravariant holds
for o1, o2 being object of B
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(Morph-Map F,((F " ) . o2),((F " ) . o1)) . ((Morph-Map (F " ),o1,o2) . m) = m
let F be reflexive feasible FunctorStr of A,B; ( F is bijective & F is coreflexive & F is Contravariant implies for o1, o2 being object of B
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(Morph-Map F,((F " ) . o2),((F " ) . o1)) . ((Morph-Map (F " ),o1,o2) . m) = m )
assume A1:
( F is bijective & F is coreflexive & F is Contravariant )
; for o1, o2 being object of B
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(Morph-Map F,((F " ) . o2),((F " ) . o1)) . ((Morph-Map (F " ),o1,o2) . m) = m
set G = F " ;
A2:
F " is Contravariant
by A1, Th40;
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; for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(Morph-Map F,((F " ) . o2),((F " ) . o1)) . ((Morph-Map (F " ),o1,o2) . m) = m
let m be Morphism of o1,o2; ( <^o1,o2^> <> {} implies (Morph-Map F,((F " ) . o2),((F " ) . o1)) . ((Morph-Map (F " ),o1,o2) . m) = m )
assume A8:
<^o1,o2^> <> {}
; (Morph-Map F,((F " ) . o2),((F " ) . o1)) . ((Morph-Map (F " ),o1,o2) . m) = m
A9:
[((F " ) . o2),((F " ) . o1)] 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 " ) . o2),((F " ) . o1)] in dom the MorphMap of F
by ZFMISC_1:106;
then A12:
Morph-Map F,((F " ) . o2),((F " ) . o1) 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 . o2),(H . o1)
by A2, Th24
.=
<^(H . o2),(H . o1)^>
by ALTCAT_1:def 2
;
then A13:
(the Arrows of A * the ObjectMap of (F " )) . [o1,o2] <> {}
by A2, A8, Def20;
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 . o2),(H . o1)]
by A2, Th24
.=
(Morph-Map F,((F " ) . o2),((F " ) . o1)) "
by A4, A6, A7, A9, MSUALG_3:def 5
;
thus (Morph-Map F,((F " ) . o2),((F " ) . o1)) . ((Morph-Map (F " ),o1,o2) . m) =
((Morph-Map F,((F " ) . o2),((F " ) . o1)) * (Morph-Map (F " ),o1,o2)) . m
by A8, A14, FUNCT_1:23
.=
(id (rng (Morph-Map F,((F " ) . o2),((F " ) . o1)))) . 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
; verum