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

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