let A, B be non empty transitive with_units AltCatStr ; :: thesis: for F being reflexive feasible FunctorStr of 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 of 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 of 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