let A, B be non empty transitive with_units AltCatStr ; :: thesis: for F being reflexive feasible FunctorStr over A,B st F is coreflexive & F is bijective holds
for a being Object of A
for b being Object of B holds
( F . a = b iff (F ") . b = a )
let F be reflexive feasible FunctorStr over A,B; :: thesis: ( F is coreflexive & F is bijective implies for a being Object of A
for b being Object of B holds
( F . a = b iff (F ") . b = a ) )
assume A1: ( F is coreflexive & F is bijective ) ; :: thesis: for a being Object of A
for b being Object of B holds
( F . a = b iff (F ") . b = a )
reconsider G = F " as reflexive feasible FunctorStr over B,A by A1, FUNCTOR0:35, FUNCTOR0:36;
let a be Object of A; :: thesis: for b being Object of B holds
( F . a = b iff (F ") . b = a )
let b be Object of B; :: thesis: ( F . a = b iff (F ") . b = a )
(F ") * F = id A by A1, FUNCTOR1:19;
then a = ((F ") * F) . a by FUNCTOR0:29;
hence ( F . a = b implies (F ") . b = a ) by FUNCTOR0:33; :: thesis: ( (F ") . b = a implies F . a = b )
F * G = id B by A1, FUNCTOR1:18;
then b = (F * G) . b by FUNCTOR0:29;
hence ( (F ") . b = a implies F . a = b ) by FUNCTOR0:33; :: thesis: verum