let A, B be category; :: thesis: for F being contravariant Functor of A,B st F is bijective holds

for G being contravariant Functor of B,A st ( for b being Object of B holds F . (G . b) = b ) & ( for a, b being Object of B st <^a,b^> <> {} holds

for f being Morphism of a,b holds F . (G . f) = f ) holds

FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "

let F be contravariant Functor of A,B; :: thesis: ( F is bijective implies for G being contravariant Functor of B,A st ( for b being Object of B holds F . (G . b) = b ) & ( for a, b being Object of B st <^a,b^> <> {} holds

for f being Morphism of a,b holds F . (G . f) = f ) holds

FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " )

assume A1: F is bijective ; :: thesis: for G being contravariant Functor of B,A st ( for b being Object of B holds F . (G . b) = b ) & ( for a, b being Object of B st <^a,b^> <> {} holds

for f being Morphism of a,b holds F . (G . f) = f ) holds

FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "

let G be contravariant Functor of B,A; :: thesis: ( ( for b being Object of B holds F . (G . b) = b ) & ( for a, b being Object of B st <^a,b^> <> {} holds

for f being Morphism of a,b holds F . (G . f) = f ) implies FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " )

assume that

A2: for b being Object of B holds F . (G . b) = b and

A3: for a, b being Object of B st <^a,b^> <> {} holds

for f being Morphism of a,b holds F . (G . f) = f ; :: thesis: FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "

for G being contravariant Functor of B,A st ( for b being Object of B holds F . (G . b) = b ) & ( for a, b being Object of B st <^a,b^> <> {} holds

for f being Morphism of a,b holds F . (G . f) = f ) holds

FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "

let F be contravariant Functor of A,B; :: thesis: ( F is bijective implies for G being contravariant Functor of B,A st ( for b being Object of B holds F . (G . b) = b ) & ( for a, b being Object of B st <^a,b^> <> {} holds

for f being Morphism of a,b holds F . (G . f) = f ) holds

FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " )

assume A1: F is bijective ; :: thesis: for G being contravariant Functor of B,A st ( for b being Object of B holds F . (G . b) = b ) & ( for a, b being Object of B st <^a,b^> <> {} holds

for f being Morphism of a,b holds F . (G . f) = f ) holds

FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "

let G be contravariant Functor of B,A; :: thesis: ( ( for b being Object of B holds F . (G . b) = b ) & ( for a, b being Object of B st <^a,b^> <> {} holds

for f being Morphism of a,b holds F . (G . f) = f ) implies FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " )

assume that

A2: for b being Object of B holds F . (G . b) = b and

A3: for a, b being Object of B st <^a,b^> <> {} holds

for f being Morphism of a,b holds F . (G . f) = f ; :: thesis: FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "

A4: now :: thesis: for a, b being Object of B st <^a,b^> <> {} holds

for f being Morphism of a,b holds (F * G) . f = (id B) . f

for f being Morphism of a,b holds (F * G) . f = (id B) . f

let a, b be Object of B; :: thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds (F * G) . f = (id B) . f )

assume A5: <^a,b^> <> {} ; :: thesis: for f being Morphism of a,b holds (F * G) . f = (id B) . f

let f be Morphism of a,b; :: thesis: (F * G) . f = (id B) . f

thus (F * G) . f = F . (G . f) by A5, FUNCTOR3:7

.= f by A3, A5

.= (id B) . f by A5, FUNCTOR0:31 ; :: thesis: verum

end;assume A5: <^a,b^> <> {} ; :: thesis: for f being Morphism of a,b holds (F * G) . f = (id B) . f

let f be Morphism of a,b; :: thesis: (F * G) . f = (id B) . f

thus (F * G) . f = F . (G . f) by A5, FUNCTOR3:7

.= f by A3, A5

.= (id B) . f by A5, FUNCTOR0:31 ; :: thesis: verum

now :: thesis: for b being Object of B holds (F * G) . b = (id B) . b

hence
FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "
by A1, A4, Th4, YELLOW18:1; :: thesis: verumlet b be Object of B; :: thesis: (F * G) . b = (id B) . b

thus (F * G) . b = F . (G . b) by FUNCTOR0:33

.= b by A2

.= (id B) . b by FUNCTOR0:29 ; :: thesis: verum

end;thus (F * G) . b = F . (G . b) by FUNCTOR0:33

.= b by A2

.= (id B) . b by FUNCTOR0:29 ; :: thesis: verum