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 A3, FUNCTOR0:def 18;

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 A1, FUNCTOR1:19;

then f = (G * F) . f by A2, A3, FUNCTOR0:31;

hence ( F . f = g implies G . g = f ) by A3, FUNCTOR3:6; :: thesis: ( G . g = f implies F . f = g )

F * G = id B by A1, A2, FUNCTOR1:18;

then g = (F * G) . g by A4, FUNCTOR0:31;

hence ( G . g = f implies F . f = g ) by A4, A5, FUNCTOR3:6; :: thesis: verum

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 A3, FUNCTOR0:def 18;

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 A1, FUNCTOR1:19;

then f = (G * F) . f by A2, A3, FUNCTOR0:31;

hence ( F . f = g implies G . g = f ) by A3, FUNCTOR3:6; :: thesis: ( G . g = f implies F . f = g )

F * G = id B by A1, A2, FUNCTOR1:18;

then g = (F * G) . g by A4, FUNCTOR0:31;

hence ( G . g = f implies F . f = g ) by A4, A5, FUNCTOR3:6; :: thesis: verum