let A be non empty AltCatStr ; :: thesis: for B, C being non empty reflexive AltCatStr

for F being feasible Covariant FunctorStr over A,B

for N being feasible Contravariant FunctorStr over B,C

for o1, o2 being Object of A

for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds

(N * F) . m = N . (F . m)

let B, C be non empty reflexive AltCatStr ; :: thesis: for F being feasible Covariant FunctorStr over A,B

for N being feasible Contravariant FunctorStr over B,C

for o1, o2 being Object of A

for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds

(N * F) . m = N . (F . m)

let F be feasible Covariant FunctorStr over A,B; :: thesis: for N being feasible Contravariant FunctorStr over B,C

for o1, o2 being Object of A

for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds

(N * F) . m = N . (F . m)

let N be feasible Contravariant FunctorStr over B,C; :: thesis: for o1, o2 being Object of A

for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds

(N * F) . m = N . (F . m)

let o1, o2 be Object of A; :: thesis: for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds

(N * F) . m = N . (F . m)

let m be Morphism of o1,o2; :: thesis: ( <^o1,o2^> <> {} implies (N * F) . m = N . (F . m) )

set I = the carrier of A;

reconsider s = the MorphMap of F . (o1,o2) as Function ;

reconsider r = (( the MorphMap of N * the ObjectMap of F) ** the MorphMap of F) . (o1,o2) as Function ;

reconsider t = ( the MorphMap of N * the ObjectMap of F) . (o1,o2) as Function ;

A1: dom (( the MorphMap of N * the ObjectMap of F) ** the MorphMap of F) = (dom ( the MorphMap of N * the ObjectMap of F)) /\ (dom the MorphMap of F) by PBOOLE:def 19

.= [: the carrier of A, the carrier of A:] /\ (dom the MorphMap of F) by PARTFUN1:def 2

.= [: the carrier of A, the carrier of A:] /\ [: the carrier of A, the carrier of A:] by PARTFUN1:def 2

.= [: the carrier of A, the carrier of A:] ;

A2: dom the ObjectMap of F = [: the carrier of A, the carrier of A:] by FUNCT_2:def 1;

A3: [o1,o2] in [: the carrier of A, the carrier of A:] by ZFMISC_1:def 2;

assume A4: <^o1,o2^> <> {} ; :: thesis: (N * F) . m = N . (F . m)

then A5: <^(F . o1),(F . o2)^> <> {} by FUNCTOR0:def 18;

then A6: dom (Morph-Map (F,o1,o2)) = <^o1,o2^> by FUNCT_2:def 1;

A7: <^(N . (F . o2)),(N . (F . o1))^> <> {} by A5, FUNCTOR0:def 19;

( (N * F) . o1 = N . (F . o1) & (N * F) . o2 = N . (F . o2) ) by FUNCTOR0:33;

hence (N * F) . m = (Morph-Map ((N * F),o1,o2)) . m by A4, A7, FUNCTOR0:def 16

.= r . m by FUNCTOR0:def 36

.= (t * s) . m by A1, A3, PBOOLE:def 19

.= t . ((Morph-Map (F,o1,o2)) . m) by A4, A6, FUNCT_1:13

.= t . (F . m) by A4, A5, FUNCTOR0:def 15

.= ( the MorphMap of N . ( the ObjectMap of F . (o1,o2))) . (F . m) by A2, A3, FUNCT_1:13

.= (Morph-Map (N,(F . o1),(F . o2))) . (F . m) by FUNCTOR0:22

.= N . (F . m) by A5, A7, FUNCTOR0:def 16 ;

:: thesis: verum

for F being feasible Covariant FunctorStr over A,B

for N being feasible Contravariant FunctorStr over B,C

for o1, o2 being Object of A

for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds

(N * F) . m = N . (F . m)

let B, C be non empty reflexive AltCatStr ; :: thesis: for F being feasible Covariant FunctorStr over A,B

for N being feasible Contravariant FunctorStr over B,C

for o1, o2 being Object of A

for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds

(N * F) . m = N . (F . m)

let F be feasible Covariant FunctorStr over A,B; :: thesis: for N being feasible Contravariant FunctorStr over B,C

for o1, o2 being Object of A

for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds

(N * F) . m = N . (F . m)

let N be feasible Contravariant FunctorStr over B,C; :: thesis: for o1, o2 being Object of A

for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds

(N * F) . m = N . (F . m)

let o1, o2 be Object of A; :: thesis: for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds

(N * F) . m = N . (F . m)

let m be Morphism of o1,o2; :: thesis: ( <^o1,o2^> <> {} implies (N * F) . m = N . (F . m) )

set I = the carrier of A;

reconsider s = the MorphMap of F . (o1,o2) as Function ;

reconsider r = (( the MorphMap of N * the ObjectMap of F) ** the MorphMap of F) . (o1,o2) as Function ;

reconsider t = ( the MorphMap of N * the ObjectMap of F) . (o1,o2) as Function ;

A1: dom (( the MorphMap of N * the ObjectMap of F) ** the MorphMap of F) = (dom ( the MorphMap of N * the ObjectMap of F)) /\ (dom the MorphMap of F) by PBOOLE:def 19

.= [: the carrier of A, the carrier of A:] /\ (dom the MorphMap of F) by PARTFUN1:def 2

.= [: the carrier of A, the carrier of A:] /\ [: the carrier of A, the carrier of A:] by PARTFUN1:def 2

.= [: the carrier of A, the carrier of A:] ;

A2: dom the ObjectMap of F = [: the carrier of A, the carrier of A:] by FUNCT_2:def 1;

A3: [o1,o2] in [: the carrier of A, the carrier of A:] by ZFMISC_1:def 2;

assume A4: <^o1,o2^> <> {} ; :: thesis: (N * F) . m = N . (F . m)

then A5: <^(F . o1),(F . o2)^> <> {} by FUNCTOR0:def 18;

then A6: dom (Morph-Map (F,o1,o2)) = <^o1,o2^> by FUNCT_2:def 1;

A7: <^(N . (F . o2)),(N . (F . o1))^> <> {} by A5, FUNCTOR0:def 19;

( (N * F) . o1 = N . (F . o1) & (N * F) . o2 = N . (F . o2) ) by FUNCTOR0:33;

hence (N * F) . m = (Morph-Map ((N * F),o1,o2)) . m by A4, A7, FUNCTOR0:def 16

.= r . m by FUNCTOR0:def 36

.= (t * s) . m by A1, A3, PBOOLE:def 19

.= t . ((Morph-Map (F,o1,o2)) . m) by A4, A6, FUNCT_1:13

.= t . (F . m) by A4, A5, FUNCTOR0:def 15

.= ( the MorphMap of N . ( the ObjectMap of F . (o1,o2))) . (F . m) by A2, A3, FUNCT_1:13

.= (Morph-Map (N,(F . o1),(F . o2))) . (F . m) by FUNCTOR0:22

.= N . (F . m) by A5, A7, FUNCTOR0:def 16 ;

:: thesis: verum