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 comp-reversing & F is Contravariant & F is coreflexive holds
F " is comp-reversing
let F be reflexive feasible FunctorStr of A,B; :: thesis: ( F is bijective & F is comp-reversing & F is Contravariant & F is coreflexive implies F " is comp-reversing )
assume A1: ( F is bijective & F is comp-reversing & F is Contravariant & F is coreflexive ) ; :: thesis: F " is comp-reversing
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 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, Def39;
A6: F is injective by A1, Def36;
then F is one-to-one by Def34;
then A7: the ObjectMap of F is one-to-one by Def7;
F is faithful by A6, Def34;
then A8: the MorphMap of F is "1-1" by Def31;
F is surjective by A1, Def36;
then F is full by Def35;
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" ) by Def33;
let o1, o2, o3 be object of B; :: according to FUNCTOR0:def 23 :: thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies for f being Morphism of o1,o2
for g being Morphism of o2,o3 ex f' being Morphism of ((F " ) . o2),((F " ) . o1) ex g' being Morphism of ((F " ) . o3),((F " ) . o2) st
( f' = (Morph-Map (F " ),o1,o2) . f & g' = (Morph-Map (F " ),o2,o3) . g & (Morph-Map (F " ),o1,o3) . (g * f) = f' * g' ) )
assume A10: <^o1,o2^> <> {} ; :: thesis: ( not <^o2,o3^> <> {} or for f being Morphism of o1,o2
for g being Morphism of o2,o3 ex f' being Morphism of ((F " ) . o2),((F " ) . o1) ex g' being Morphism of ((F " ) . o3),((F " ) . o2) st
( f' = (Morph-Map (F " ),o1,o2) . f & g' = (Morph-Map (F " ),o2,o3) . g & (Morph-Map (F " ),o1,o3) . (g * f) = f' * g' ) )
then A11: <^(H . o2),(H . o1)^> <> {} by A2, Def20;
assume A12: <^o2,o3^> <> {} ; :: thesis: for f being Morphism of o1,o2
for g being Morphism of o2,o3 ex f' being Morphism of ((F " ) . o2),((F " ) . o1) ex g' being Morphism of ((F " ) . o3),((F " ) . o2) st
( f' = (Morph-Map (F " ),o1,o2) . f & g' = (Morph-Map (F " ),o2,o3) . g & (Morph-Map (F " ),o1,o3) . (g * f) = f' * g' )
then A13: <^(H . o3),(H . o2)^> <> {} by A2, Def20;
A14: <^o1,o3^> <> {} by A10, A12, ALTCAT_1:def 4;
then A15: <^(H . o3),(H . o1)^> <> {} by A2, Def20;
then A16: <^(F . ((F " ) . o1)),(F . ((F " ) . o3))^> <> {} by A1, Def20;
let f be Morphism of o1,o2; :: thesis: for g being Morphism of o2,o3 ex f' being Morphism of ((F " ) . o2),((F " ) . o1) ex g' being Morphism of ((F " ) . o3),((F " ) . o2) st
( f' = (Morph-Map (F " ),o1,o2) . f & g' = (Morph-Map (F " ),o2,o3) . g & (Morph-Map (F " ),o1,o3) . (g * f) = f' * g' )
let g be Morphism of o2,o3; :: thesis: ex f' being Morphism of ((F " ) . o2),((F " ) . o1) ex g' being Morphism of ((F " ) . o3),((F " ) . o2) st
( f' = (Morph-Map (F " ),o1,o2) . f & g' = (Morph-Map (F " ),o2,o3) . g & (Morph-Map (F " ),o1,o3) . (g * f) = f' * g' )
reconsider K = F " as Contravariant FunctorStr of B,A by A1, Th40;
K . f = (Morph-Map K,o1,o2) . f by A10, A11, Def17;
then reconsider f' = (Morph-Map K,o1,o2) . f as Morphism of ((F " ) . o2),((F " ) . o1) ;
K . g = (Morph-Map K,o2,o3) . g by A12, A13, Def17;
then reconsider g' = (Morph-Map K,o2,o3) . g as Morphism of ((F " ) . o3),((F " ) . o2) ;
take f' ; :: thesis: ex g' being Morphism of ((F " ) . o3),((F " ) . o2) st
( f' = (Morph-Map (F " ),o1,o2) . f & g' = (Morph-Map (F " ),o2,o3) . g & (Morph-Map (F " ),o1,o3) . (g * f) = f' * g' )
take g' ; :: thesis: ( f' = (Morph-Map (F " ),o1,o2) . f & g' = (Morph-Map (F " ),o2,o3) . g & (Morph-Map (F " ),o1,o3) . (g * f) = f' * g' )
thus f' = (Morph-Map (F " ),o1,o2) . f ; :: thesis: ( g' = (Morph-Map (F " ),o2,o3) . g & (Morph-Map (F " ),o1,o3) . (g * f) = f' * g' )
thus g' = (Morph-Map (F " ),o2,o3) . g ; :: thesis: (Morph-Map (F " ),o1,o3) . (g * f) = f' * g'
consider g'' being Morphism of (F . ((F " ) . o2)),(F . ((F " ) . o3)), f'' being Morphism of (F . ((F " ) . o1)),(F . ((F " ) . o2)) such that
A17: g'' = (Morph-Map F,((F " ) . o3),((F " ) . o2)) . g' and
A18: f'' = (Morph-Map F,((F " ) . o2),((F " ) . o1)) . f' and
A19: (Morph-Map F,((F " ) . o3),((F " ) . o1)) . (f' * g') = g'' * f'' by A1, A11, A13, Def23;
A20: g = g'' by A1, A12, A17, Th42;
A21: f = f'' by A1, A10, A18, Th42;
A22: [((F " ) . o3),((F " ) . o1)] in [:the carrier of A,the carrier of A:] by ZFMISC_1:106;
A23: [o1,o3] in [:the carrier of B,the carrier of B:] by ZFMISC_1:106;
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 4;
then [((F " ) . o3),((F " ) . o1)] in dom the MorphMap of F by ZFMISC_1:106;
then A25: Morph-Map F,((F " ) . o3),((F " ) . o1) is one-to-one by A8, MSUALG_3:def 2;
[((F " ) . o3),((F " ) . o1)] in dom the ObjectMap of F by A22, FUNCT_2:def 1;
then A26: (the Arrows of B * the ObjectMap of F) . [((F " ) . o3),((F " ) . o1)] = the Arrows of B . (the ObjectMap of F . ((F " ) . o3),((F " ) . o1)) by FUNCT_1:23
.= the Arrows of B . (F . ((F " ) . o1)),(F . ((F " ) . o3)) by A1, Th24
.= <^(F . ((F " ) . o1)),(F . ((F " ) . o3))^> by ALTCAT_1:def 2 ;
Morph-Map F,((F " ) . o3),((F " ) . o1) is Function of (the Arrows of A . [((F " ) . o3),((F " ) . o1)]),((the Arrows of B * the ObjectMap of F) . [((F " ) . o3),((F " ) . o1)]) by A4, A22, PBOOLE:def 18;
then A27: dom (Morph-Map F,((F " ) . o3),((F " ) . o1)) = the Arrows of A . ((F " ) . o3),((F " ) . o1) by A16, A26, FUNCT_2:def 1
.= <^((F " ) . o3),((F " ) . o1)^> by ALTCAT_1:def 2 ;
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:23
.= the Arrows of A . ((F " ) . o3),((F " ) . o1) by A2, Th24
.= <^((F " ) . o3),((F " ) . o1)^> by ALTCAT_1:def 2 ;
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,o3 is Function of (the Arrows of B . [o1,o3]),((the Arrows of A * the ObjectMap of (F " )) . [o1,o3]) by A23, PBOOLE:def 18;
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 2 ;
A30: Morph-Map (F " ),o1,o3 = (ff "" ) . (the ObjectMap of (F " ) . o1,o3) by A3, A5, A24, FUNCT_1:23
.= (ff "" ) . [(H . o3),(H . o1)] by A2, Th24
.= (Morph-Map F,((F " ) . o3),((F " ) . o1)) " by A4, A8, A9, A22, MSUALG_3:def 5 ;
A31: the ObjectMap of (F * H) = the ObjectMap of F * the ObjectMap of H by Def37
.= the ObjectMap of F * (the ObjectMap of F " ) by A1, Def39
.= id (rng the ObjectMap of F) by A7, FUNCT_1:61
.= id (dom the ObjectMap of (F " )) by A3, A7, FUNCT_1:55
.= 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:106;
then A32: the ObjectMap of (F * H) . o1,o1 = [o1,o1] by A31, FUNCT_1:35;
A33: F . ((F " ) . o1) = (F * H) . o1 by Th34
.= o1 by A32, MCART_1:7 ;
[o2,o2] in [:the carrier of B,the carrier of B:] by ZFMISC_1:106;
then A34: the ObjectMap of (F * H) . o2,o2 = [o2,o2] by A31, FUNCT_1:35;
A35: F . ((F " ) . o2) = (F * H) . o2 by Th34
.= o2 by A34, MCART_1:7 ;
[o3,o3] in [:the carrier of B,the carrier of B:] by ZFMISC_1:106;
then A36: the ObjectMap of (F * H) . o3,o3 = [o3,o3] by A31, FUNCT_1:35;
A37: F . ((F " ) . o3) = (F * H) . o3 by Th34
.= o3 by A36, MCART_1:7 ;
(Morph-Map (F " ),o1,o3) . (g * f) in rng (Morph-Map (F " ),o1,o3) by A14, A29, FUNCT_1:def 5;
then A38: (Morph-Map (F " ),o1,o3) . (g * f) in dom (Morph-Map F,((F " ) . o3),((F " ) . o1)) by A25, A30, FUNCT_1:55;
(Morph-Map F,((F " ) . o3),((F " ) . o1)) . ((Morph-Map (F " ),o1,o3) . (g * f)) = (Morph-Map F,((F " ) . o3),((F " ) . o1)) . (f' * g') by A1, A14, A19, A20, A21, A33, A35, A37, Th42;
hence (Morph-Map (F " ),o1,o3) . (g * f) = f' * g' by A25, A27, A38, FUNCT_1:def 8; :: thesis: verum