let A, B be non empty transitive with_units AltCatStr ; :: thesis: for F being feasible Covariant FunctorStr of A,B
for G being feasible Covariant FunctorStr of 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 of A,B; :: thesis: for G being feasible Covariant FunctorStr of 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 of 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 A1: ( F is bijective & 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 A2: <^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 )
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:22;
then f = (G * F) . f by A1, A2, FUNCTOR0:32;
hence ( F . f = g implies G . g = f ) by A2, FUNCTOR3:6; :: thesis: ( G . g = f implies F . f = g )
A3: <^(F . a1),(F . a2)^> <> {} by A2, FUNCTOR0:def 19;
F is surjective by A1, FUNCTOR0:def 36;
then F is onto by FUNCTOR0:def 35;
then ( F is reflexive & F is coreflexive ) by FUNCTOR0:45;
then A4: ( G . (F . a1) = a1 & G . (F . a2) = a2 ) by A1, Th1;
F * G = id B by A1, FUNCTOR1:21;
then g = (F * G) . g by A3, FUNCTOR0:32;
hence ( G . g = f implies F . f = g ) by A3, A4, FUNCTOR3:6; :: thesis: verum