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 coreflexive holds
F " is reflexive
let F be reflexive feasible FunctorStr over A,B; ( F is bijective & F is coreflexive implies F " is reflexive )
assume that
A1:
F is bijective
and
A2:
F is coreflexive
; F " is reflexive
set G = F " ;
A3:
the ObjectMap of (F ") = the ObjectMap of F "
by A1, Def38;
let o be Object of B; FUNCTOR0:def 10 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
; verum