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 holds
F " is reflexive
let F be reflexive feasible FunctorStr of A,B; :: thesis: ( F is bijective & F is coreflexive implies F " is reflexive )
assume that
A1: F is bijective and
A2: F is coreflexive ; :: thesis: F " is reflexive
set G = F " ;
A3: the ObjectMap of (F " ) = the ObjectMap of F " by A1, Def39;
let o be object of B; :: according to FUNCTOR0:def 11 :: thesis: the ObjectMap of (F " ) . o,o = [((F " ) . o),((F " ) . o)]
A4: dom the ObjectMap of F = [:the carrier of A,the carrier of A:] by FUNCT_2:def 1;
consider p being object of A such that
A5: o = F . p by A2, Th21;
F is injective by A1, Def36;
then F is one-to-one by Def34;
then A6: the ObjectMap of F is one-to-one by Def7;
A7: [p,p] in dom the ObjectMap of F by A4, ZFMISC_1:106;
A8: (F " ) . (F . p) = ((F " ) * F) . p by Th34
.= ((the ObjectMap of (F " ) * the ObjectMap of F) . p,p) `1 by Def37
.= ((id (dom the ObjectMap of F)) . [p,p]) `1 by A3, A6, FUNCT_1:61
.= [p,p] `1 by A7, FUNCT_1:35
.= p by MCART_1:7 ;
thus the ObjectMap of (F " ) . o,o = the ObjectMap of (F " ) . (the ObjectMap of F . p,p) by A5, Def11
.= (the ObjectMap of (F " ) * the ObjectMap of F) . [p,p] by A7, FUNCT_1:23
.= (id (dom the ObjectMap of F)) . [p,p] by A3, A6, FUNCT_1:61
.= [((F " ) . o),((F " ) . o)] by A5, A7, A8, FUNCT_1:35 ; :: thesis: verum