let A, B be non empty transitive with_units AltCatStr ; for F being reflexive feasible FunctorStr over A,B st F is bijective & F is comp-preserving & F is Covariant & F is coreflexive holds
F " is comp-preserving
let F be reflexive feasible FunctorStr over A,B; ( F is bijective & F is comp-preserving & F is Covariant & F is coreflexive implies F " is comp-preserving )
assume A1:
( F is bijective & F is comp-preserving & F is Covariant & F is coreflexive )
; F " is comp-preserving
set G = F " ;
A2:
F " is Covariant
by A1, Th38;
reconsider H = F " as reflexive feasible FunctorStr over B,A by A1, Th35, Th36;
A3:
the ObjectMap of (F ") = the ObjectMap of F "
by A1, Def38;
consider ff being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F such that
A4:
ff = the MorphMap of F
and
A5:
the MorphMap of (F ") = (ff "") * ( the ObjectMap of F ")
by A1, Def38;
A6:
F is injective
by A1;
then
F is one-to-one
;
then A7:
the ObjectMap of F is one-to-one
;
F is faithful
by A6;
then A8:
the MorphMap of F is "1-1"
;
F is surjective
by A1;
then
F is full
;
then A9:
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" )
;
let o1, o2, o3 be Object of B; FUNCTOR0:def 21 ( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies for f being Morphism of o1,o2
for g being Morphism of o2,o3 ex f9 being Morphism of ((F ") . o1),((F ") . o2) ex g9 being Morphism of ((F ") . o2),((F ") . o3) st
( f9 = (Morph-Map ((F "),o1,o2)) . f & g9 = (Morph-Map ((F "),o2,o3)) . g & (Morph-Map ((F "),o1,o3)) . (g * f) = g9 * f9 ) )
assume A10:
<^o1,o2^> <> {}
; ( not <^o2,o3^> <> {} or for f being Morphism of o1,o2
for g being Morphism of o2,o3 ex f9 being Morphism of ((F ") . o1),((F ") . o2) ex g9 being Morphism of ((F ") . o2),((F ") . o3) st
( f9 = (Morph-Map ((F "),o1,o2)) . f & g9 = (Morph-Map ((F "),o2,o3)) . g & (Morph-Map ((F "),o1,o3)) . (g * f) = g9 * f9 ) )
then A11:
<^(H . o1),(H . o2)^> <> {}
by A2, Def18;
assume A12:
<^o2,o3^> <> {}
; for f being Morphism of o1,o2
for g being Morphism of o2,o3 ex f9 being Morphism of ((F ") . o1),((F ") . o2) ex g9 being Morphism of ((F ") . o2),((F ") . o3) st
( f9 = (Morph-Map ((F "),o1,o2)) . f & g9 = (Morph-Map ((F "),o2,o3)) . g & (Morph-Map ((F "),o1,o3)) . (g * f) = g9 * f9 )
then A13:
<^(H . o2),(H . o3)^> <> {}
by A2, Def18;
A14:
<^o1,o3^> <> {}
by A10, A12, ALTCAT_1:def 2;
then A15:
<^(H . o1),(H . o3)^> <> {}
by A2, Def18;
then A16:
<^(F . ((F ") . o1)),(F . ((F ") . o3))^> <> {}
by A1, Def18;
let f be Morphism of o1,o2; for g being Morphism of o2,o3 ex f9 being Morphism of ((F ") . o1),((F ") . o2) ex g9 being Morphism of ((F ") . o2),((F ") . o3) st
( f9 = (Morph-Map ((F "),o1,o2)) . f & g9 = (Morph-Map ((F "),o2,o3)) . g & (Morph-Map ((F "),o1,o3)) . (g * f) = g9 * f9 )
let g be Morphism of o2,o3; ex f9 being Morphism of ((F ") . o1),((F ") . o2) ex g9 being Morphism of ((F ") . o2),((F ") . o3) st
( f9 = (Morph-Map ((F "),o1,o2)) . f & g9 = (Morph-Map ((F "),o2,o3)) . g & (Morph-Map ((F "),o1,o3)) . (g * f) = g9 * f9 )
reconsider K = F " as Covariant FunctorStr over B,A by A1, Th38;
K . f = (Morph-Map (K,o1,o2)) . f
by A10, A11, Def15;
then reconsider f9 = (Morph-Map (K,o1,o2)) . f as Morphism of ((F ") . o1),((F ") . o2) ;
K . g = (Morph-Map (K,o2,o3)) . g
by A12, A13, Def15;
then reconsider g9 = (Morph-Map (K,o2,o3)) . g as Morphism of ((F ") . o2),((F ") . o3) ;
take
f9
; ex g9 being Morphism of ((F ") . o2),((F ") . o3) st
( f9 = (Morph-Map ((F "),o1,o2)) . f & g9 = (Morph-Map ((F "),o2,o3)) . g & (Morph-Map ((F "),o1,o3)) . (g * f) = g9 * f9 )
take
g9
; ( f9 = (Morph-Map ((F "),o1,o2)) . f & g9 = (Morph-Map ((F "),o2,o3)) . g & (Morph-Map ((F "),o1,o3)) . (g * f) = g9 * f9 )
thus
f9 = (Morph-Map ((F "),o1,o2)) . f
; ( g9 = (Morph-Map ((F "),o2,o3)) . g & (Morph-Map ((F "),o1,o3)) . (g * f) = g9 * f9 )
thus
g9 = (Morph-Map ((F "),o2,o3)) . g
; (Morph-Map ((F "),o1,o3)) . (g * f) = g9 * f9
consider f99 being Morphism of (F . ((F ") . o1)),(F . ((F ") . o2)), g99 being Morphism of (F . ((F ") . o2)),(F . ((F ") . o3)) such that
A17:
f99 = (Morph-Map (F,((F ") . o1),((F ") . o2))) . f9
and
A18:
g99 = (Morph-Map (F,((F ") . o2),((F ") . o3))) . g9
and
A19:
(Morph-Map (F,((F ") . o1),((F ") . o3))) . (g9 * f9) = g99 * f99
by A1, A11, A13;
A20:
g = g99
by A1, A12, A18, Th40;
A21:
f = f99
by A1, A10, A17, Th40;
A22:
[((F ") . o1),((F ") . o3)] in [: the carrier of A, the carrier of A:]
by ZFMISC_1:87;
A23:
[o1,o3] in [: the carrier of B, the carrier of B:]
by ZFMISC_1:87;
then A24:
[o1,o3] 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 2;
then
[((F ") . o1),((F ") . o3)] in dom the MorphMap of F
by ZFMISC_1:87;
then A25:
Morph-Map (F,((F ") . o1),((F ") . o3)) is one-to-one
by A8;
[((F ") . o1),((F ") . o3)] in dom the ObjectMap of F
by A22, FUNCT_2:def 1;
then A26: ( the Arrows of B * the ObjectMap of F) . [((F ") . o1),((F ") . o3)] =
the Arrows of B . ( the ObjectMap of F . (((F ") . o1),((F ") . o3)))
by FUNCT_1:13
.=
the Arrows of B . ((F . ((F ") . o1)),(F . ((F ") . o3)))
by A1, Th22
.=
<^(F . ((F ") . o1)),(F . ((F ") . o3))^>
by ALTCAT_1:def 1
;
Morph-Map (F,((F ") . o1),((F ") . o3)) is Function of ( the Arrows of A . [((F ") . o1),((F ") . o3)]),(( the Arrows of B * the ObjectMap of F) . [((F ") . o1),((F ") . o3)])
by A4, A22, PBOOLE:def 15;
then A27: dom (Morph-Map (F,((F ") . o1),((F ") . o3))) =
the Arrows of A . (((F ") . o1),((F ") . o3))
by A16, A26, FUNCT_2:def 1
.=
<^((F ") . o1),((F ") . o3)^>
by ALTCAT_1:def 1
;
A28: ( the Arrows of A * the ObjectMap of (F ")) . [o1,o3] =
the Arrows of A . ( the ObjectMap of H . (o1,o3))
by A24, FUNCT_1:13
.=
the Arrows of A . (((F ") . o1),((F ") . o3))
by A2, Th22
.=
<^((F ") . o1),((F ") . o3)^>
by ALTCAT_1:def 1
;
the MorphMap of (F ") is ManySortedFunction of the Arrows of B, the Arrows of A * the ObjectMap of (F ")
by Def4;
then
Morph-Map ((F "),o1,o3) is Function of ( the Arrows of B . [o1,o3]),(( the Arrows of A * the ObjectMap of (F ")) . [o1,o3])
by A23, PBOOLE:def 15;
then A29: dom (Morph-Map ((F "),o1,o3)) =
the Arrows of B . (o1,o3)
by A15, A28, FUNCT_2:def 1
.=
<^o1,o3^>
by ALTCAT_1:def 1
;
A30: Morph-Map ((F "),o1,o3) =
(ff "") . ( the ObjectMap of (F ") . (o1,o3))
by A3, A5, A24, FUNCT_1:13
.=
(ff "") . [(H . o1),(H . o3)]
by A2, Th22
.=
(Morph-Map (F,((F ") . o1),((F ") . o3))) "
by A4, A8, A9, A22, MSUALG_3:def 4
;
A31: the ObjectMap of (F * H) =
the ObjectMap of F * the ObjectMap of H
by Def36
.=
the ObjectMap of F * ( the ObjectMap of F ")
by A1, Def38
.=
id (rng the ObjectMap of F)
by A7, FUNCT_1:39
.=
id (dom the ObjectMap of (F "))
by A3, A7, FUNCT_1:33
.=
id [: the carrier of B, the carrier of B:]
by FUNCT_2:def 1
;
[o1,o1] in [: the carrier of B, the carrier of B:]
by ZFMISC_1:87;
then A32:
the ObjectMap of (F * H) . (o1,o1) = [o1,o1]
by A31, FUNCT_1:18;
A33: F . ((F ") . o1) =
(F * H) . o1
by Th33
.=
o1
by A32
;
[o2,o2] in [: the carrier of B, the carrier of B:]
by ZFMISC_1:87;
then A34:
the ObjectMap of (F * H) . (o2,o2) = [o2,o2]
by A31, FUNCT_1:18;
A35: F . ((F ") . o2) =
(F * H) . o2
by Th33
.=
o2
by A34
;
[o3,o3] in [: the carrier of B, the carrier of B:]
by ZFMISC_1:87;
then A36:
the ObjectMap of (F * H) . (o3,o3) = [o3,o3]
by A31, FUNCT_1:18;
A37: F . ((F ") . o3) =
(F * H) . o3
by Th33
.=
o3
by A36
;
(Morph-Map ((F "),o1,o3)) . (g * f) in rng (Morph-Map ((F "),o1,o3))
by A14, A29, FUNCT_1:def 3;
then A38:
(Morph-Map ((F "),o1,o3)) . (g * f) in dom (Morph-Map (F,((F ") . o1),((F ") . o3)))
by A25, A30, FUNCT_1:33;
(Morph-Map (F,((F ") . o1),((F ") . o3))) . ((Morph-Map ((F "),o1,o3)) . (g * f)) = (Morph-Map (F,((F ") . o1),((F ") . o3))) . (g9 * f9)
by A1, A14, A19, A20, A21, A33, A35, A37, Th40;
hence
(Morph-Map ((F "),o1,o3)) . (g * f) = g9 * f9
by A25, A27, A38; verum