let A, B be non empty transitive with_units reflexive AltCatStr ; :: thesis: for F being feasible FunctorStr over A,B st F is bijective holds

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

set CCA = [: the carrier of A, the carrier of A:];

set CCB = [: the carrier of B, the carrier of B:];

let F be feasible FunctorStr over A,B; :: thesis: ( F is bijective implies (F ") " = FunctorStr(# the ObjectMap of F, the MorphMap of F #) )

assume A1: F is bijective ; :: thesis: (F ") " = FunctorStr(# the ObjectMap of F, the MorphMap of F #)

A2: F is injective by A1;

then F is one-to-one ;

then A3: the ObjectMap of F is one-to-one ;

A4: F " is bijective by A1, FUNCTOR0:35;

then F " is surjective ;

then A5: F " is full ;

F " is injective by A4;

then A6: F " is faithful ;

A7: the ObjectMap of (F ") " = ( the ObjectMap of F ") " by A1, FUNCTOR0:def 38

.= the ObjectMap of F by A3, FUNCT_1:43 ;

F is faithful by A2;

then A8: the MorphMap of F is "1-1" ;

A9: F is surjective by A1;

then F is onto ;

then the ObjectMap of F is onto ;

then A10: rng the ObjectMap of F = [: the carrier of B, the carrier of B:] by FUNCT_2:def 3;

A11: F is full by A9;

the MorphMap of ((F ") ") = the MorphMap of F

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

set CCA = [: the carrier of A, the carrier of A:];

set CCB = [: the carrier of B, the carrier of B:];

let F be feasible FunctorStr over A,B; :: thesis: ( F is bijective implies (F ") " = FunctorStr(# the ObjectMap of F, the MorphMap of F #) )

assume A1: F is bijective ; :: thesis: (F ") " = FunctorStr(# the ObjectMap of F, the MorphMap of F #)

A2: F is injective by A1;

then F is one-to-one ;

then A3: the ObjectMap of F is one-to-one ;

A4: F " is bijective by A1, FUNCTOR0:35;

then F " is surjective ;

then A5: F " is full ;

F " is injective by A4;

then A6: F " is faithful ;

A7: the ObjectMap of (F ") " = ( the ObjectMap of F ") " by A1, FUNCTOR0:def 38

.= the ObjectMap of F by A3, FUNCT_1:43 ;

F is faithful by A2;

then A8: the MorphMap of F is "1-1" ;

A9: F is surjective by A1;

then F is onto ;

then the ObjectMap of F is onto ;

then A10: rng the ObjectMap of F = [: the carrier of B, the carrier of B:] by FUNCT_2:def 3;

A11: F is full by A9;

the MorphMap of ((F ") ") = the MorphMap of F

proof

hence
(F ") " = FunctorStr(# the ObjectMap of F, the MorphMap of F #)
by A4, A7, FUNCTOR0:def 38; :: thesis: verum
A12:
ex kk being ManySortedFunction of the Arrows of B, the Arrows of A * the ObjectMap of (F ") st

( kk = the MorphMap of (F ") & kk is "onto" ) by A5;

A13: ex k being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st

( k = the MorphMap of F & k is "onto" ) by A11;

consider f being ManySortedFunction of the Arrows of B, the Arrows of A * the ObjectMap of (F ") such that

A14: f = the MorphMap of (F ") and

A15: the MorphMap of ((F ") ") = (f "") * ( the ObjectMap of (F ") ") by A4, FUNCTOR0:def 38;

consider g being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F such that

A16: g = the MorphMap of F and

A17: the MorphMap of (F ") = (g "") * ( the ObjectMap of F ") by A1, FUNCTOR0:def 38;

A18: f is "1-1" by A6, A14;

for i being object st i in [: the carrier of A, the carrier of A:] holds

((f "") * ( the ObjectMap of (F ") ")) . i = the MorphMap of F . i

end;( kk = the MorphMap of (F ") & kk is "onto" ) by A5;

A13: ex k being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st

( k = the MorphMap of F & k is "onto" ) by A11;

consider f being ManySortedFunction of the Arrows of B, the Arrows of A * the ObjectMap of (F ") such that

A14: f = the MorphMap of (F ") and

A15: the MorphMap of ((F ") ") = (f "") * ( the ObjectMap of (F ") ") by A4, FUNCTOR0:def 38;

consider g being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F such that

A16: g = the MorphMap of F and

A17: the MorphMap of (F ") = (g "") * ( the ObjectMap of F ") by A1, FUNCTOR0:def 38;

A18: f is "1-1" by A6, A14;

for i being object st i in [: the carrier of A, the carrier of A:] holds

((f "") * ( the ObjectMap of (F ") ")) . i = the MorphMap of F . i

proof

hence
the MorphMap of ((F ") ") = the MorphMap of F
by A15; :: thesis: verum
A19:
the ObjectMap of F " is Function of [: the carrier of B, the carrier of B:],[: the carrier of A, the carrier of A:]
by A3, A10, FUNCT_2:25;

let i be object ; :: thesis: ( i in [: the carrier of A, the carrier of A:] implies ((f "") * ( the ObjectMap of (F ") ")) . i = the MorphMap of F . i )

assume A20: i in [: the carrier of A, the carrier of A:] ; :: thesis: ((f "") * ( the ObjectMap of (F ") ")) . i = the MorphMap of F . i

then A21: the ObjectMap of F . i in [: the carrier of B, the carrier of B:] by FUNCT_2:5;

the ObjectMap of F " is Function of [: the carrier of B, the carrier of B:],[: the carrier of A, the carrier of A:] by A3, A10, FUNCT_2:25;

then A22: ( the ObjectMap of F ") . ( the ObjectMap of F . i) in [: the carrier of A, the carrier of A:] by A21, FUNCT_2:5;

A23: g . i is one-to-one by A8, A16, A20, MSUALG_3:1;

((f "") * ( the ObjectMap of (F ") ")) . i = (f "") . ( the ObjectMap of F . i) by A7, A20, FUNCT_2:15

.= ( the MorphMap of (F ") . ( the ObjectMap of F . i)) " by A14, A12, A18, A21, MSUALG_3:def 4

.= ((g "") . (( the ObjectMap of F ") . ( the ObjectMap of F . i))) " by A17, A20, A19, FUNCT_2:5, FUNCT_2:15

.= ((g . (( the ObjectMap of F ") . ( the ObjectMap of F . i))) ") " by A8, A16, A13, A22, MSUALG_3:def 4

.= ((g . i) ") " by A3, A20, FUNCT_2:26

.= the MorphMap of F . i by A16, A23, FUNCT_1:43 ;

hence ((f "") * ( the ObjectMap of (F ") ")) . i = the MorphMap of F . i ; :: thesis: verum

end;let i be object ; :: thesis: ( i in [: the carrier of A, the carrier of A:] implies ((f "") * ( the ObjectMap of (F ") ")) . i = the MorphMap of F . i )

assume A20: i in [: the carrier of A, the carrier of A:] ; :: thesis: ((f "") * ( the ObjectMap of (F ") ")) . i = the MorphMap of F . i

then A21: the ObjectMap of F . i in [: the carrier of B, the carrier of B:] by FUNCT_2:5;

the ObjectMap of F " is Function of [: the carrier of B, the carrier of B:],[: the carrier of A, the carrier of A:] by A3, A10, FUNCT_2:25;

then A22: ( the ObjectMap of F ") . ( the ObjectMap of F . i) in [: the carrier of A, the carrier of A:] by A21, FUNCT_2:5;

A23: g . i is one-to-one by A8, A16, A20, MSUALG_3:1;

((f "") * ( the ObjectMap of (F ") ")) . i = (f "") . ( the ObjectMap of F . i) by A7, A20, FUNCT_2:15

.= ( the MorphMap of (F ") . ( the ObjectMap of F . i)) " by A14, A12, A18, A21, MSUALG_3:def 4

.= ((g "") . (( the ObjectMap of F ") . ( the ObjectMap of F . i))) " by A17, A20, A19, FUNCT_2:5, FUNCT_2:15

.= ((g . (( the ObjectMap of F ") . ( the ObjectMap of F . i))) ") " by A8, A16, A13, A22, MSUALG_3:def 4

.= ((g . i) ") " by A3, A20, FUNCT_2:26

.= the MorphMap of F . i by A16, A23, FUNCT_1:43 ;

hence ((f "") * ( the ObjectMap of (F ") ")) . i = the MorphMap of F . i ; :: thesis: verum