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