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 ") * F = id A

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

let F be feasible FunctorStr over A,B; :: thesis: ( F is bijective implies (F ") * F = id A )

assume A1: F is bijective ; :: thesis: (F ") * F = id A

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

A2: f = the MorphMap of F and

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

set OM = the ObjectMap of F;

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

A5: the Arrows of A is_transformable_to the Arrows of B * the ObjectMap of F

then F is faithful ;

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

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

((f "") * (id [: the carrier of A, the carrier of A:])) . i = (f "") . i

F is injective by A1;

then F is one-to-one ;

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

the ObjectMap of ((F ") * F) = the ObjectMap of (F ") * the ObjectMap of F by FUNCTOR0:def 36;

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

then A14: the ObjectMap of ((F ") * F) = id [: the carrier of A, the carrier of A:] by A13, A4, FUNCT_1:39;

F is surjective by A1;

then ( F is full & F is onto ) ;

then A15: 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" ) ;

the MorphMap of ((F ") * F) = (((f "") * ( the ObjectMap of F ")) * the ObjectMap of F) ** f by A2, A3, FUNCTOR0:def 36

.= ((f "") * (( the ObjectMap of F ") * the ObjectMap of F)) ** f by RELAT_1:36 ;

then the MorphMap of ((F ") * F) = ((f "") * (id [: the carrier of A, the carrier of A:])) ** f by A13, A4, FUNCT_1:39;

then the MorphMap of ((F ") * F) = id the Arrows of A by A5, A2, A10, A15, A12, Lm1;

hence (F ") * F = id A by A14, FUNCTOR0:def 29; :: thesis: verum

(F ") * F = id A

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

let F be feasible FunctorStr over A,B; :: thesis: ( F is bijective implies (F ") * F = id A )

assume A1: F is bijective ; :: thesis: (F ") * F = id A

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

A2: f = the MorphMap of F and

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

set OM = the ObjectMap of F;

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

A5: the Arrows of A is_transformable_to the Arrows of B * the ObjectMap of F

proof

F is injective
by A1;
let i be set ; :: according to PZFMISC1:def 3 :: thesis: ( not i in [: the carrier of A, the carrier of A:] or not ( the Arrows of B * the ObjectMap of F) . i = {} or the Arrows of A . i = {} )

assume A6: i in [: the carrier of A, the carrier of A:] ; :: thesis: ( not ( the Arrows of B * the ObjectMap of F) . i = {} or the Arrows of A . i = {} )

then consider o1, o2 being object such that

A7: ( o1 in the carrier of A & o2 in the carrier of A ) and

A8: i = [o1,o2] by ZFMISC_1:84;

reconsider o1 = o1, o2 = o2 as Object of A by A7;

A9: the Arrows of A . i = the Arrows of A . (o1,o2) by A8

.= <^o1,o2^> by ALTCAT_1:def 1 ;

assume ( the Arrows of B * the ObjectMap of F) . i = {} ; :: thesis: the Arrows of A . i = {}

then the Arrows of B . ( the ObjectMap of F . (o1,o2)) = {} by A6, A8, FUNCT_2:15;

hence the Arrows of A . i = {} by A9, FUNCTOR0:def 11; :: thesis: verum

end;assume A6: i in [: the carrier of A, the carrier of A:] ; :: thesis: ( not ( the Arrows of B * the ObjectMap of F) . i = {} or the Arrows of A . i = {} )

then consider o1, o2 being object such that

A7: ( o1 in the carrier of A & o2 in the carrier of A ) and

A8: i = [o1,o2] by ZFMISC_1:84;

reconsider o1 = o1, o2 = o2 as Object of A by A7;

A9: the Arrows of A . i = the Arrows of A . (o1,o2) by A8

.= <^o1,o2^> by ALTCAT_1:def 1 ;

assume ( the Arrows of B * the ObjectMap of F) . i = {} ; :: thesis: the Arrows of A . i = {}

then the Arrows of B . ( the ObjectMap of F . (o1,o2)) = {} by A6, A8, FUNCT_2:15;

hence the Arrows of A . i = {} by A9, FUNCTOR0:def 11; :: thesis: verum

then F is faithful ;

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

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

((f "") * (id [: the carrier of A, the carrier of A:])) . i = (f "") . i

proof

then A12:
(f "") * (id [: the carrier of A, the carrier of A:]) = f ""
;
let i be object ; :: thesis: ( i in [: the carrier of A, the carrier of A:] implies ((f "") * (id [: the carrier of A, the carrier of A:])) . i = (f "") . i )

assume A11: i in [: the carrier of A, the carrier of A:] ; :: thesis: ((f "") * (id [: the carrier of A, the carrier of A:])) . i = (f "") . i

then ((f "") * (id [: the carrier of A, the carrier of A:])) . i = (f "") . ((id [: the carrier of A, the carrier of A:]) . i) by FUNCT_2:15

.= (f "") . i by A11, FUNCT_1:18 ;

hence ((f "") * (id [: the carrier of A, the carrier of A:])) . i = (f "") . i ; :: thesis: verum

end;assume A11: i in [: the carrier of A, the carrier of A:] ; :: thesis: ((f "") * (id [: the carrier of A, the carrier of A:])) . i = (f "") . i

then ((f "") * (id [: the carrier of A, the carrier of A:])) . i = (f "") . ((id [: the carrier of A, the carrier of A:]) . i) by FUNCT_2:15

.= (f "") . i by A11, FUNCT_1:18 ;

hence ((f "") * (id [: the carrier of A, the carrier of A:])) . i = (f "") . i ; :: thesis: verum

F is injective by A1;

then F is one-to-one ;

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

the ObjectMap of ((F ") * F) = the ObjectMap of (F ") * the ObjectMap of F by FUNCTOR0:def 36;

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

then A14: the ObjectMap of ((F ") * F) = id [: the carrier of A, the carrier of A:] by A13, A4, FUNCT_1:39;

F is surjective by A1;

then ( F is full & F is onto ) ;

then A15: 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" ) ;

the MorphMap of ((F ") * F) = (((f "") * ( the ObjectMap of F ")) * the ObjectMap of F) ** f by A2, A3, FUNCTOR0:def 36

.= ((f "") * (( the ObjectMap of F ") * the ObjectMap of F)) ** f by RELAT_1:36 ;

then the MorphMap of ((F ") * F) = ((f "") * (id [: the carrier of A, the carrier of A:])) ** f by A13, A4, FUNCT_1:39;

then the MorphMap of ((F ") * F) = id the Arrows of A by A5, A2, A10, A15, A12, Lm1;

hence (F ") * F = id A by A14, FUNCTOR0:def 29; :: thesis: verum