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

for G being feasible FunctorStr over B,A st FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " holds

F * G = id B

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

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

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

F * G = id B )

assume A1: F is bijective ; :: thesis: for G being feasible FunctorStr over B,A st FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " holds

F * G = id B

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

A2: k = the MorphMap of F and

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

F is injective by A1;

then F is one-to-one ;

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

set OM = the ObjectMap of F;

F is surjective by A1;

then F is onto ;

then the ObjectMap of F is onto ;

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

F is injective by A1;

then A6: F is faithful ;

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

F is surjective by A1;

then ( F is full & F is onto ) ;

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

A8: f = the MorphMap of F and

A9: f is "onto" ;

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

assume A10: FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " ; :: thesis: F * G = id B

A11: the ObjectMap of G = the ObjectMap of F " by A1, A10, FUNCTOR0:def 38;

FunctorStr(# the ObjectMap of G, the MorphMap of G #) is bijective by A1, A10, FUNCTOR0:35;

then FunctorStr(# the ObjectMap of G, the MorphMap of G #) is surjective ;

then ( FunctorStr(# the ObjectMap of G, the MorphMap of G #) is full & FunctorStr(# the ObjectMap of G, the MorphMap of G #) is onto ) ;

then A12: the ObjectMap of G is onto ;

set OMG = the ObjectMap of G;

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

reconsider OM = the ObjectMap of F as bifunction of the carrier of A, the carrier of B ;

A14: [: the carrier of B, the carrier of B:] = dom ((f * the ObjectMap of G) ** ((k "") * the ObjectMap of G)) by PARTFUN1:def 2;

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

((f * the ObjectMap of G) ** ((k "") * the ObjectMap of G)) . i = (id the Arrows of B) . i

then A23: the MorphMap of (F * G) = id the Arrows of B by A15;

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

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

then the ObjectMap of (F * G) = id [: the carrier of B, the carrier of B:] by A4, A5, FUNCT_1:39;

hence F * G = id B by A23, FUNCTOR0:def 29; :: thesis: verum

for G being feasible FunctorStr over B,A st FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " holds

F * G = id B

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

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

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

F * G = id B )

assume A1: F is bijective ; :: thesis: for G being feasible FunctorStr over B,A st FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " holds

F * G = id B

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

A2: k = the MorphMap of F and

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

F is injective by A1;

then F is one-to-one ;

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

set OM = the ObjectMap of F;

F is surjective by A1;

then F is onto ;

then the ObjectMap of F is onto ;

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

F is injective by A1;

then A6: F is faithful ;

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

F is surjective by A1;

then ( F is full & F is onto ) ;

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

A8: f = the MorphMap of F and

A9: f is "onto" ;

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

assume A10: FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " ; :: thesis: F * G = id B

A11: the ObjectMap of G = the ObjectMap of F " by A1, A10, FUNCTOR0:def 38;

FunctorStr(# the ObjectMap of G, the MorphMap of G #) is bijective by A1, A10, FUNCTOR0:35;

then FunctorStr(# the ObjectMap of G, the MorphMap of G #) is surjective ;

then ( FunctorStr(# the ObjectMap of G, the MorphMap of G #) is full & FunctorStr(# the ObjectMap of G, the MorphMap of G #) is onto ) ;

then A12: the ObjectMap of G is onto ;

set OMG = the ObjectMap of G;

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

reconsider OM = the ObjectMap of F as bifunction of the carrier of A, the carrier of B ;

A14: [: the carrier of B, the carrier of B:] = dom ((f * the ObjectMap of G) ** ((k "") * the ObjectMap of G)) by PARTFUN1:def 2;

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

((f * the ObjectMap of G) ** ((k "") * the ObjectMap of G)) . i = (id the Arrows of B) . i

proof

the MorphMap of (F * G) = (f * the ObjectMap of G) ** ((k "") * the ObjectMap of G)
by A10, A3, A8, A11, FUNCTOR0:def 36;
let i be object ; :: thesis: ( i in [: the carrier of B, the carrier of B:] implies ((f * the ObjectMap of G) ** ((k "") * the ObjectMap of G)) . i = (id the Arrows of B) . i )

assume A16: i in [: the carrier of B, the carrier of B:] ; :: thesis: ((f * the ObjectMap of G) ** ((k "") * the ObjectMap of G)) . i = (id the Arrows of B) . i

A17: dom the ObjectMap of G = [: the carrier of B, the carrier of B:] by FUNCT_2:def 1;

then A18: (f * the ObjectMap of G) . i = k . ( the ObjectMap of G . i) by A2, A8, A16, FUNCT_1:13;

rng the ObjectMap of G = [: the carrier of A, the carrier of A:] by A12, FUNCT_2:def 3;

then A19: the ObjectMap of G . i in [: the carrier of A, the carrier of A:] by A16, A17, FUNCT_1:def 3;

then A20: rng (f . ( the ObjectMap of G . i)) = ( the Arrows of B * the ObjectMap of F) . ( the ObjectMap of G . i) by A9

.= the Arrows of B . ( the ObjectMap of F . ( the ObjectMap of G . i)) by A13, A19, FUNCT_1:13 ;

A21: the ObjectMap of F . ( the ObjectMap of G . i) = (OM * (OM ")) . i by A11, A16, A17, FUNCT_1:13

.= (id [: the carrier of B, the carrier of B:]) . i by A4, A5, FUNCT_1:39

.= i by A16, FUNCT_1:18 ;

( f is "1-1" & dom f = [: the carrier of A, the carrier of A:] ) by A6, A8, PARTFUN1:def 2;

then A22: f . ( the ObjectMap of G . i) is one-to-one by A19;

((k "") * the ObjectMap of G) . i = (k "") . ( the ObjectMap of G . i) by A16, A17, FUNCT_1:13

.= (k . ( the ObjectMap of G . i)) " by A7, A2, A8, A9, A19, MSUALG_3:def 4 ;

then ((f * the ObjectMap of G) ** ((k "") * the ObjectMap of G)) . i = (f . ( the ObjectMap of G . i)) * ((f . ( the ObjectMap of G . i)) ") by A2, A8, A14, A16, A18, PBOOLE:def 19

.= id ( the Arrows of B . i) by A22, A20, A21, FUNCT_1:39

.= (id the Arrows of B) . i by A16, MSUALG_3:def 1 ;

hence ((f * the ObjectMap of G) ** ((k "") * the ObjectMap of G)) . i = (id the Arrows of B) . i ; :: thesis: verum

end;assume A16: i in [: the carrier of B, the carrier of B:] ; :: thesis: ((f * the ObjectMap of G) ** ((k "") * the ObjectMap of G)) . i = (id the Arrows of B) . i

A17: dom the ObjectMap of G = [: the carrier of B, the carrier of B:] by FUNCT_2:def 1;

then A18: (f * the ObjectMap of G) . i = k . ( the ObjectMap of G . i) by A2, A8, A16, FUNCT_1:13;

rng the ObjectMap of G = [: the carrier of A, the carrier of A:] by A12, FUNCT_2:def 3;

then A19: the ObjectMap of G . i in [: the carrier of A, the carrier of A:] by A16, A17, FUNCT_1:def 3;

then A20: rng (f . ( the ObjectMap of G . i)) = ( the Arrows of B * the ObjectMap of F) . ( the ObjectMap of G . i) by A9

.= the Arrows of B . ( the ObjectMap of F . ( the ObjectMap of G . i)) by A13, A19, FUNCT_1:13 ;

A21: the ObjectMap of F . ( the ObjectMap of G . i) = (OM * (OM ")) . i by A11, A16, A17, FUNCT_1:13

.= (id [: the carrier of B, the carrier of B:]) . i by A4, A5, FUNCT_1:39

.= i by A16, FUNCT_1:18 ;

( f is "1-1" & dom f = [: the carrier of A, the carrier of A:] ) by A6, A8, PARTFUN1:def 2;

then A22: f . ( the ObjectMap of G . i) is one-to-one by A19;

((k "") * the ObjectMap of G) . i = (k "") . ( the ObjectMap of G . i) by A16, A17, FUNCT_1:13

.= (k . ( the ObjectMap of G . i)) " by A7, A2, A8, A9, A19, MSUALG_3:def 4 ;

then ((f * the ObjectMap of G) ** ((k "") * the ObjectMap of G)) . i = (f . ( the ObjectMap of G . i)) * ((f . ( the ObjectMap of G . i)) ") by A2, A8, A14, A16, A18, PBOOLE:def 19

.= id ( the Arrows of B . i) by A22, A20, A21, FUNCT_1:39

.= (id the Arrows of B) . i by A16, MSUALG_3:def 1 ;

hence ((f * the ObjectMap of G) ** ((k "") * the ObjectMap of G)) . i = (id the Arrows of B) . i ; :: thesis: verum

then A23: the MorphMap of (F * G) = id the Arrows of B by A15;

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

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

then the ObjectMap of (F * G) = id [: the carrier of B, the carrier of B:] by A4, A5, FUNCT_1:39;

hence F * G = id B by A23, FUNCTOR0:def 29; :: thesis: verum