let A, B be non empty transitive with_units AltCatStr ; :: thesis: for F being reflexive feasible FunctorStr over A,B st F is bijective & F is coreflexive holds
F " is reflexive
let F be reflexive feasible FunctorStr over 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, Def38;
let o be Object of B; :: according to FUNCTOR0:def 10 :: 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, Th20;
F is injective by A1;
then F is one-to-one ;
then A6: the ObjectMap of F is one-to-one ;
A7: [p,p] in dom the ObjectMap of F by A4, ZFMISC_1:87;
A8: (F ") . (F . p) = ((F ") * F) . p by Th33
.= (( the ObjectMap of (F ") * the ObjectMap of F) . (p,p)) `1 by Def36
.= ((id (dom the ObjectMap of F)) . [p,p]) `1 by A3, A6, FUNCT_1:39
.= [p,p] `1 by A7, FUNCT_1:18
.= p ;
thus the ObjectMap of (F ") . (o,o) = the ObjectMap of (F ") . ( the ObjectMap of F . (p,p)) by A5, Def10
.= ( the ObjectMap of (F ") * the ObjectMap of F) . [p,p] by A7, FUNCT_1:13
.= (id (dom the ObjectMap of F)) . [p,p] by A3, A6, FUNCT_1:39
.= [((F ") . o),((F ") . o)] by A5, A7, A8, FUNCT_1:18 ; :: thesis: verum