let A, B be non empty transitive with_units AltCatStr ; :: thesis: for F being feasible FunctorStr over A,B st F is bijective holds
( F " is bijective & F " is feasible )
let F be feasible FunctorStr over A,B; :: thesis: ( F is bijective implies ( F " is bijective & F " is feasible ) )
assume A1: F is bijective ; :: thesis: ( F " is bijective & F " is feasible )
set G = F " ;
A2: the ObjectMap of (F ") = the ObjectMap of F " by A1, Def38;
A3: F is injective by A1;
then F is one-to-one ;
then A4: the ObjectMap of F is one-to-one ;
hence the ObjectMap of (F ") is one-to-one by A2; :: according to FUNCTOR0:def 6,FUNCTOR0:def 33,FUNCTOR0:def 35 :: thesis: ( F " is faithful & F " is surjective & F " is feasible )
F is faithful by A3;
then A5: the MorphMap of F is "1-1" ;
A6: F is surjective by A1;
then F is onto ;
then A7: the ObjectMap of F is onto ;
consider h being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F such that
A8: h = the MorphMap of F and
A9: the MorphMap of (F ") = (h "") * ( the ObjectMap of F ") by A1, Def38;
F is full by A6;
then A10: ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st
( f = the MorphMap of F & f is "onto" ) ;
set AA = [: the carrier of A, the carrier of A:];
set BB = [: the carrier of B, the carrier of B:];
A11: rng the ObjectMap of F = [: the carrier of B, the carrier of B:] by A7;
reconsider f = the MorphMap of (F ") as ManySortedFunction of the Arrows of B, the Arrows of A * the ObjectMap of (F ") by Def4;
f is "1-1"

proof

let i be set ; :: according to MSUALG_3:def 2 :: thesis: for b₁ being set holds
( not i in proj1 f or not f . i = b₁ or b₁ is one-to-one )
let g be Function; :: thesis: ( not i in proj1 f or not f . i = g or g is one-to-one )
assume that
A12: i in dom f and
A13: f . i = g ; :: thesis: g is one-to-one
i in [: the carrier of B, the carrier of B:] by A12;
then A14: i in dom ( the ObjectMap of F ") by A4, A11, FUNCT_1:33;
then ( the ObjectMap of F ") . i in rng ( the ObjectMap of F ") by FUNCT_1:def 3;
then A15: ( the ObjectMap of F ") . i in dom the ObjectMap of F by A4, FUNCT_1:33;
then ( the ObjectMap of F ") . i in [: the carrier of A, the carrier of A:] ;
then ( the ObjectMap of F ") . i in dom h by PARTFUN1:def 2;
then A16: h . (( the ObjectMap of F ") . i) is one-to-one by A5, A8;
g = (h "") . (( the ObjectMap of F ") . i) by A9, A13, A14, FUNCT_1:13
.= (h . (( the ObjectMap of F ") . i)) " by A5, A8, A10, A15, MSUALG_3:def 4 ;
hence g is one-to-one by A16; :: thesis: verum

end;

hence the MorphMap of (F ") is "1-1" ; :: according to FUNCTOR0:def 30 :: thesis: ( F " is surjective & F " is feasible )
thus F " is full :: according to FUNCTOR0:def 34 :: thesis: ( F " is onto & F " is feasible )

proof

take f ; :: according to FUNCTOR0:def 32 :: thesis: ( f = the MorphMap of (F ") & f is "onto" )
thus f = the MorphMap of (F ") ; :: thesis: f is "onto"
let i be set ; :: according to MSUALG_3:def 3 :: thesis: ( not i in [: the carrier of B, the carrier of B:] or proj2 (f . i) = ( the Arrows of A * the ObjectMap of (F ")) . i )
assume A17: i in [: the carrier of B, the carrier of B:] ; :: thesis: proj2 (f . i) = ( the Arrows of A * the ObjectMap of (F ")) . i
then A18: i in dom the ObjectMap of (F ") by FUNCT_2:def 1;
A19: i in dom ( the ObjectMap of F ") by A4, A11, A17, FUNCT_1:33;
then ( the ObjectMap of F ") . i in rng ( the ObjectMap of F ") by FUNCT_1:def 3;
then A20: ( the ObjectMap of F ") . i in dom the ObjectMap of F by A4, FUNCT_1:33;
then ( the ObjectMap of F ") . i in [: the carrier of A, the carrier of A:] ;
then the ObjectMap of (F ") . i in dom h by A2, PARTFUN1:def 2;
then A21: h . ( the ObjectMap of (F ") . i) is one-to-one by A5, A8;
set j = the ObjectMap of (F ") . i;
A22: h . ( the ObjectMap of (F ") . i) is Function of ( the Arrows of A . ( the ObjectMap of (F ") . i)),(( the Arrows of B * the ObjectMap of F) . ( the ObjectMap of (F ") . i)) by A2, A20, PBOOLE:def 15;
consider o1, o2 being Element of A such that
A23: the ObjectMap of (F ") . i = [o1,o2] by A2, A20, DOMAIN_1:1;
reconsider o1 = o1, o2 = o2 as Object of A ;

A24: now :: thesis: ( the Arrows of A . ( the ObjectMap of (F ") . i) <> {} implies ( the Arrows of B * the ObjectMap of F) . ( the ObjectMap of (F ") . i) <> {} )

assume the Arrows of A . ( the ObjectMap of (F ") . i) <> {} ; :: thesis: ( the Arrows of B * the ObjectMap of F) . ( the ObjectMap of (F ") . i) <> {}
then the Arrows of A . (o1,o2) <> {} by A23;
then <^o1,o2^> <> {} by ALTCAT_1:def 1;
then the Arrows of B . ( the ObjectMap of F . (o1,o2)) <> {} by Def11;
hence ( the Arrows of B * the ObjectMap of F) . ( the ObjectMap of (F ") . i) <> {} by A2, A20, A23, FUNCT_1:13; :: thesis: verum

end;

f . i = (h "") . (( the ObjectMap of F ") . i) by A9, A19, FUNCT_1:13
.= (h . (( the ObjectMap of F ") . i)) " by A5, A8, A10, A20, MSUALG_3:def 4 ;
hence rng (f . i) = dom (h . ( the ObjectMap of (F ") . i)) by A2, A21, FUNCT_1:33
.= the Arrows of A . ( the ObjectMap of (F ") . i) by A22, A24, FUNCT_2:def 1
.= ( the Arrows of A * the ObjectMap of (F ")) . i by A18, FUNCT_1:13 ;
:: thesis: verum

end;

thus rng the ObjectMap of (F ") = dom the ObjectMap of F by A2, A4, FUNCT_1:33
.= [: the carrier of A, the carrier of A:] by FUNCT_2:def 1 ; :: according to FUNCT_2:def 3,FUNCTOR0:def 7 :: thesis: F " is feasible
let o1, o2 be Object of B; :: according to FUNCTOR0:def 11 :: thesis: ( <^o1,o2^> <> {} implies the Arrows of A . ( the ObjectMap of (F ") . (o1,o2)) <> {} )
assume <^o1,o2^> <> {} ; :: thesis: the Arrows of A . ( the ObjectMap of (F ") . (o1,o2)) <> {}
then A25: the Arrows of B . (o1,o2) <> {} by ALTCAT_1:def 1;
A26: [o1,o2] in [: the carrier of B, the carrier of B:] by ZFMISC_1:87;
then consider p1, p2 being Element of A such that
A27: the ObjectMap of (F ") . [o1,o2] = [p1,p2] by DOMAIN_1:1, FUNCT_2:5;
reconsider p1 = p1, p2 = p2 as Object of A ;
[o1,o2] in dom the ObjectMap of (F ") by A26, FUNCT_2:def 1;
then A28: the ObjectMap of F . (p1,p2) = ( the ObjectMap of F * the ObjectMap of (F ")) . [o1,o2] by A27, FUNCT_1:13
.= (id [: the carrier of B, the carrier of B:]) . [o1,o2] by A2, A4, A11, FUNCT_1:39
.= [o1,o2] by A26, FUNCT_1:18 ;
assume A29: the Arrows of A . ( the ObjectMap of (F ") . (o1,o2)) = {} ; :: thesis: contradiction
A30: [p1,p2] in [: the carrier of A, the carrier of A:] by ZFMISC_1:87;
then A31: [p1,p2] in dom the ObjectMap of F by FUNCT_2:def 1;
h . [p1,p2] is Function of ( the Arrows of A . [p1,p2]),(( the Arrows of B * the ObjectMap of F) . [p1,p2]) by A30, PBOOLE:def 15;
then {} = rng (h . [p1,p2]) by A27, A29
.= ( the Arrows of B * the ObjectMap of F) . [p1,p2] by A8, A10, A30
.= the Arrows of B . [o1,o2] by A28, A31, FUNCT_1:13 ;
hence contradiction by A25; :: thesis: verum