let A, B be non empty transitive with_units AltCatStr ; :: thesis: for F being feasible FunctorStr of A,B st F is bijective holds
( F " is bijective & F " is feasible )
let F be feasible FunctorStr of 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, Def39;
A3: F is injective by A1, Def36;
then F is one-to-one by Def34;
then A4: the ObjectMap of F is one-to-one by Def7;
hence the ObjectMap of (F " ) is one-to-one by A2; :: according to FUNCTOR0:def 7,FUNCTOR0:def 34,FUNCTOR0:def 36 :: thesis: ( F " is faithful & F " is surjective & F " is feasible )
F is faithful by A3, Def34;
then A5: the MorphMap of F is "1-1" by Def31;
A6: F is surjective by A1, Def36;
then F is onto by Def35;
then A7: the ObjectMap of F is onto by Def8;
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, Def39;
F is full by A6, Def35;
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" ) by Def33;
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, FUNCT_2:def 3;
reconsider f = the MorphMap of (F " ) as ManySortedFunction of the Arrows of B,the Arrows of A * the ObjectMap of (F " ) by Def5;
f is "1-1"

proof

let i be set ; :: according to MSUALG_3:def 2 :: thesis: for b₁ being set holds
( not i in dom f or not f . i = b₁ or b₁ is one-to-one )
let g be Function; :: thesis: ( not i in dom 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, PARTFUN1:def 4;
then A14: i in dom (the ObjectMap of F " ) by A4, A11, FUNCT_1:55;
then (the ObjectMap of F " ) . i in rng (the ObjectMap of F " ) by FUNCT_1:def 5;
then A15: (the ObjectMap of F " ) . i in dom the ObjectMap of F by A4, FUNCT_1:55;
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 4;
then A16: h . ((the ObjectMap of F " ) . i) is one-to-one by A5, A8, MSUALG_3:def 2;
g = (h "" ) . ((the ObjectMap of F " ) . i) by A9, A13, A14, FUNCT_1:23
.= (h . ((the ObjectMap of F " ) . i)) " by A5, A8, A10, A15, MSUALG_3:def 5 ;
hence g is one-to-one by A16; :: thesis: verum

end;

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

proof

take f ; :: according to FUNCTOR0:def 33 :: 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 rng (f . i) = (the Arrows of A * the ObjectMap of (F " )) . i )
assume A17: i in [:the carrier of B,the carrier of B:] ; :: thesis: rng (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:55;
then (the ObjectMap of F " ) . i in rng (the ObjectMap of F " ) by FUNCT_1:def 5;
then A20: (the ObjectMap of F " ) . i in dom the ObjectMap of F by A4, FUNCT_1:55;
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 4;
then A21: h . (the ObjectMap of (F " ) . i) is one-to-one by A5, A8, MSUALG_3:def 2;
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 18;
consider o1, o2 being Element of A such that
A23: the ObjectMap of (F " ) . i = [o1,o2] by A2, A20, DOMAIN_1:9;
reconsider o1 = o1, o2 = o2 as object of A ;

A24: now

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 2;
then the Arrows of B . (the ObjectMap of F . o1,o2) <> {} by Def12;
hence (the Arrows of B * the ObjectMap of F) . (the ObjectMap of (F " ) . i) <> {} by A2, A20, A23, FUNCT_1:23; :: thesis: verum

end;

f . i = (h "" ) . ((the ObjectMap of F " ) . i) by A9, A19, FUNCT_1:23
.= (h . ((the ObjectMap of F " ) . i)) " by A5, A8, A10, A20, MSUALG_3:def 5 ;
hence rng (f . i) = dom (h . (the ObjectMap of (F " ) . i)) by A2, A21, FUNCT_1:55
.= 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:23 ;
:: thesis: verum

end;

thus rng the ObjectMap of (F " ) = dom the ObjectMap of F by A2, A4, FUNCT_1:55
.= [:the carrier of A,the carrier of A:] by FUNCT_2:def 1 ; :: according to FUNCT_2:def 3,FUNCTOR0:def 8 :: thesis: F " is feasible
let o1, o2 be object of B; :: according to FUNCTOR0:def 12 :: 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 2;
A26: [o1,o2] in [:the carrier of B,the carrier of B:] by ZFMISC_1:106;
then the ObjectMap of (F " ) . [o1,o2] in [:the carrier of A,the carrier of A:] by FUNCT_2:7;
then consider p1, p2 being Element of A such that
A27: the ObjectMap of (F " ) . [o1,o2] = [p1,p2] by DOMAIN_1:9;
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:23
.= (id [:the carrier of B,the carrier of B:]) . [o1,o2] by A2, A4, A11, FUNCT_1:61
.= [o1,o2] by A26, FUNCT_1:35 ;
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:106;
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 18;
then dom (h . [p1,p2]) = {} by A27, A29;
then {} = rng (h . [p1,p2]) by RELAT_1:65
.= (the Arrows of B * the ObjectMap of F) . [p1,p2] by A8, A10, A30, MSUALG_3:def 3
.= the Arrows of B . [o1,o2] by A28, A31, FUNCT_1:23 ;
hence contradiction by A25; :: thesis: verum