let A, B be non empty transitive with_units AltCatStr ; :: thesis: for F being feasible Covariant FunctorStr over A,B
for G being feasible Covariant FunctorStr over B,A st F is bijective & G = F " holds
for a1, a2 being Object of A st <^a1,a2^> <> {} holds
for f being Morphism of a1,a2
for g being Morphism of (F . a1),(F . a2) holds
( F . f = g iff G . g = f )

let F be feasible Covariant FunctorStr over A,B; :: thesis: for G being feasible Covariant FunctorStr over B,A st F is bijective & G = F " holds
for a1, a2 being Object of A st <^a1,a2^> <> {} holds
for f being Morphism of a1,a2
for g being Morphism of (F . a1),(F . a2) holds
( F . f = g iff G . g = f )

let G be feasible Covariant FunctorStr over B,A; :: thesis: ( F is bijective & G = F " implies for a1, a2 being Object of A st <^a1,a2^> <> {} holds
for f being Morphism of a1,a2
for g being Morphism of (F . a1),(F . a2) holds
( F . f = g iff G . g = f ) )

assume that
A1: F is bijective and
A2: G = F " ; :: thesis: for a1, a2 being Object of A st <^a1,a2^> <> {} holds
for f being Morphism of a1,a2
for g being Morphism of (F . a1),(F . a2) holds
( F . f = g iff G . g = f )

let a1, a2 be Object of A; :: thesis: ( <^a1,a2^> <> {} implies for f being Morphism of a1,a2
for g being Morphism of (F . a1),(F . a2) holds
( F . f = g iff G . g = f ) )

assume A3: <^a1,a2^> <> {} ; :: thesis: for f being Morphism of a1,a2
for g being Morphism of (F . a1),(F . a2) holds
( F . f = g iff G . g = f )

A4: <^(F . a1),(F . a2)^> <> {} by ;
F is surjective by A1;
then F is onto ;
then ( F is reflexive & F is coreflexive ) by FUNCTOR0:44;
then A5: ( G . (F . a1) = a1 & G . (F . a2) = a2 ) by A1, A2, Th1;
let f be Morphism of a1,a2; :: thesis: for g being Morphism of (F . a1),(F . a2) holds
( F . f = g iff G . g = f )

let g be Morphism of (F . a1),(F . a2); :: thesis: ( F . f = g iff G . g = f )
(F ") * F = id A by ;
then f = (G * F) . f by ;
hence ( F . f = g implies G . g = f ) by ; :: thesis: ( G . g = f implies F . f = g )
F * G = id B by ;
then g = (F * G) . g by ;
hence ( G . g = f implies F . f = g ) by ; :: thesis: verum