let A, B be non empty transitive with_units AltCatStr ; :: thesis: for F being feasible Contravariant FunctorStr over A,B
for G being feasible Contravariant 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 . a2),(F . a1) holds
( F . f = g iff G . g = f )
let F be feasible Contravariant FunctorStr over A,B; :: thesis: for G being feasible Contravariant 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 . a2),(F . a1) holds
( F . f = g iff G . g = f )
let G be feasible Contravariant 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 . a2),(F . a1) 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 . a2),(F . a1) 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 . a2),(F . a1) 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 . a2),(F . a1) holds
( F . f = g iff G . g = f )
A4: <^(F . a2),(F . a1)^> <> {} by A3, FUNCTOR0:def 19;
F is surjective by A1;
then F is onto ;
then ( F is reflexive & F is coreflexive ) by FUNCTOR0:45;
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 . a2),(F . a1) holds
( F . f = g iff G . g = f )
let g be Morphism of (F . a2),(F . a1); :: 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:7; :: 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:7; :: thesis: verum