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 )
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:22;
then a = ((F " ) * F) . a by FUNCTOR0:30;
hence ( F . a = b implies (F " ) . b = a ) by FUNCTOR0:34; :: thesis: ( (F " ) . b = a implies F . a = b )
reconsider G = F " as reflexive feasible FunctorStr of B,A by A1, FUNCTOR0:36, FUNCTOR0:37;
F * G = id B by A1, FUNCTOR1:21;
then b = (F * G) . b by FUNCTOR0:30;
hence ( (F " ) . b = a implies F . a = b ) by FUNCTOR0:34; :: thesis: verum