:: FUNCTOR1 semantic presentation

begin


registration
cluster non empty transitive with_units reflexive for AltCatStr ;
existence
 ex b1 being non empty AltCatStr st
( b1 is transitive & b1 is with_units & b1 is reflexive )
proof
set C = the category;
take  the category ; ::_thesis: ( the category is transitive & the category is with_units & the category is reflexive )
thus  ( the category is transitive & the category is with_units & the category is reflexive ) ; ::_thesis: verum
end;
end;

registration
let A be non empty reflexive AltCatStr ;
cluster non empty reflexive for SubCatStr of A;
existence
 ex b1 being SubCatStr of A st
( not b1 is empty & b1 is reflexive )
proof
reconsider B = A as SubCatStr of A by ALTCAT_2:20;
take  B ; ::_thesis: ( not B is empty & B is reflexive )
thus  ( not B is empty & B is reflexive ) ; ::_thesis: verum
end;
end;

registration
let C1, C2 be non empty reflexive AltCatStr ;
let F be feasible FunctorStr over C1,C2;
let A be non empty reflexive SubCatStr of C1;
clusterF | A ->  feasible ;
coherence
 F | A is feasible ;
end;

begin

registration
let X be set ;
cluster id X ->  onto ;
coherence
 id X is onto
proof
reconsider f = id X as Function of X,X ;
 rng f = X by RELAT_1:45;
hence  id X is onto by FUNCT_2:def_3; ::_thesis: verum
end;
end;

theorem :: FUNCTOR1:1
for A being non empty set
for B, C being non empty Subset of A
for D being non empty Subset of B st C = D holds
incl C = (incl B) * (incl D)
proof
let A be non empty set ; ::_thesis: for B, C being non empty Subset of A
for D being non empty Subset of B st C = D holds
incl C = (incl B) * (incl D)
let B, C be non empty Subset of A; ::_thesis: for D being non empty Subset of B st C = D holds
incl C = (incl B) * (incl D)
let D be non empty Subset of B; ::_thesis: ( C = D implies incl C = (incl B) * (incl D) )
assume A1: C = D ; ::_thesis: incl C = (incl B) * (incl D)
(incl B) * (incl D) = id (B /\ D) by FUNCT_1:22
.= incl C by A1, XBOOLE_1:28 ;
hence  incl C = (incl B) * (incl D) ; ::_thesis: verum
end;

theorem Th2: :: FUNCTOR1:2
for X, Y being set
for f being Function of X,Y st f is bijective holds
f " is Function of Y,X
proof
let X, Y be set ; ::_thesis: for f being Function of X,Y st f is bijective holds
f " is Function of Y,X
let f be Function of X,Y; ::_thesis: ( f is bijective implies f " is Function of Y,X )
assume A1: f is bijective ; ::_thesis: f " is Function of Y,X
then  rng f = Y by FUNCT_2:def_3;
hence  f " is Function of Y,X by A1, FUNCT_2:25; ::_thesis: verum
end;

theorem :: FUNCTOR1:3
for X, Y being set
for Z being non empty set
for f being Function of X,Y
for g being Function of Y,Z st f is bijective & g is bijective holds
ex h being Function of X,Z st
( h = g * f & h is bijective )
proof
let X, Y be set ; ::_thesis: for Z being non empty set
for f being Function of X,Y
for g being Function of Y,Z st f is bijective & g is bijective holds
ex h being Function of X,Z st
( h = g * f & h is bijective )
let Z be non empty set ; ::_thesis: for f being Function of X,Y
for g being Function of Y,Z st f is bijective & g is bijective holds
ex h being Function of X,Z st
( h = g * f & h is bijective )
let f be Function of X,Y; ::_thesis: for g being Function of Y,Z st f is bijective & g is bijective holds
ex h being Function of X,Z st
( h = g * f & h is bijective )
let g be Function of Y,Z; ::_thesis: ( f is bijective & g is bijective implies ex h being Function of X,Z st
( h = g * f & h is bijective ) )
assume that
A1: f is bijective and
A2: g is bijective ; ::_thesis: ex h being Function of X,Z st
( h = g * f & h is bijective )
A3: rng g = Z by A2, FUNCT_2:def_3;
then  ( Y = {} iff Z = {} ) ;
then reconsider h = g * f as Function of X,Z ;
take  h ; ::_thesis: ( h = g * f & h is bijective )
 rng f = Y by A1, FUNCT_2:def_3;
then  rng (g * f) = Z by A3, FUNCT_2:14;
then  h is onto by FUNCT_2:def_3;
hence  ( h = g * f & h is bijective ) by A1, A2; ::_thesis: verum
end;

begin

theorem Th4: :: FUNCTOR1:4
for A being non empty reflexive AltCatStr
for B being non empty reflexive SubCatStr of A
for C being non empty SubCatStr of A
for D being non empty SubCatStr of B st C = D holds
incl C = (incl B) * (incl D)
proof
let A be non empty reflexive AltCatStr ; ::_thesis: for B being non empty reflexive SubCatStr of A
for C being non empty SubCatStr of A
for D being non empty SubCatStr of B st C = D holds
incl C = (incl B) * (incl D)
let B be non empty reflexive SubCatStr of A; ::_thesis: for C being non empty SubCatStr of A
for D being non empty SubCatStr of B st C = D holds
incl C = (incl B) * (incl D)
let C be non empty SubCatStr of A; ::_thesis: for D being non empty SubCatStr of B st C = D holds
incl C = (incl B) * (incl D)
let D be non empty SubCatStr of B; ::_thesis: ( C = D implies incl C = (incl B) * (incl D) )
assume A1: C = D ; ::_thesis: incl C = (incl B) * (incl D)
set X = [: the carrier of B, the carrier of B:];
set Y = [: the carrier of D, the carrier of D:];
A2: the carrier of D c= the carrier of B by ALTCAT_2:def_11;
then A3: [: the carrier of D, the carrier of D:] c= [: the carrier of B, the carrier of B:] by ZFMISC_1:96;
 for i being set st i in [: the carrier of D, the carrier of D:] holds
the MorphMap of (incl C) . i = (( the MorphMap of (incl B) * the ObjectMap of (incl D)) ** the MorphMap of (incl D)) . i
proof
set dom2 = dom the MorphMap of (incl D);
set dom1 = dom ( the MorphMap of (incl B) * the ObjectMap of (incl D));
set XX = the Arrows of B;
set YY = the Arrows of D;
let i be set ; ::_thesis: ( i in [: the carrier of D, the carrier of D:] implies the MorphMap of (incl C) . i = (( the MorphMap of (incl B) * the ObjectMap of (incl D)) ** the MorphMap of (incl D)) . i )
A4: the MorphMap of (incl C) . i = (id the Arrows of C) . i by FUNCTOR0:def_28;
A5: ( dom (( the MorphMap of (incl B) * the ObjectMap of (incl D)) ** the MorphMap of (incl D)) = (dom the MorphMap of (incl D)) /\ (dom ( the MorphMap of (incl B) * the ObjectMap of (incl D))) & dom the MorphMap of (incl D) = [: the carrier of D, the carrier of D:] ) by PARTFUN1:def_2, PBOOLE:def_19;
A6: dom ( the MorphMap of (incl B) * the ObjectMap of (incl D)) = dom ( the MorphMap of (incl B) * (id [: the carrier of D, the carrier of D:])) by FUNCTOR0:def_28
.= (dom the MorphMap of (incl B)) /\ [: the carrier of D, the carrier of D:] by FUNCT_1:19
.= [: the carrier of B, the carrier of B:] /\ [: the carrier of D, the carrier of D:] by PARTFUN1:def_2
.= [: the carrier of D, the carrier of D:] by A2, XBOOLE_1:28, ZFMISC_1:96 ;
assume A7: i in [: the carrier of D, the carrier of D:] ; ::_thesis: the MorphMap of (incl C) . i = (( the MorphMap of (incl B) * the ObjectMap of (incl D)) ** the MorphMap of (incl D)) . i
then A8: i in dom (id [: the carrier of D, the carrier of D:]) ;
 the Arrows of D cc= the Arrows of B by ALTCAT_2:def_11;
then A9: the Arrows of D . i c= the Arrows of B . i by A7, ALTCAT_2:def_2;
A10: ( the MorphMap of (incl B) * the ObjectMap of (incl D)) . i = ( the MorphMap of (incl B) * (id [: the carrier of D, the carrier of D:])) . i by FUNCTOR0:def_28
.= the MorphMap of (incl B) . ((id [: the carrier of D, the carrier of D:]) . i) by A8, FUNCT_1:13
.= the MorphMap of (incl B) . i by A7, FUNCT_1:18 ;
 ( the MorphMap of (incl B) . i = (id the Arrows of B) . i & the MorphMap of (incl D) . i = (id the Arrows of D) . i ) by FUNCTOR0:def_28;
then ( the MorphMap of (incl B) . i) * ( the MorphMap of (incl D) . i) = ((id the Arrows of B) . i) * (id ( the Arrows of D . i)) by A7, MSUALG_3:def_1
.= (id ( the Arrows of B . i)) * (id ( the Arrows of D . i)) by A3, A7, MSUALG_3:def_1
.= id (( the Arrows of B . i) /\ ( the Arrows of D . i)) by FUNCT_1:22
.= id ( the Arrows of D . i) by A9, XBOOLE_1:28
.= the MorphMap of (incl C) . i by A1, A7, A4, MSUALG_3:def_1 ;
hence  the MorphMap of (incl C) . i = (( the MorphMap of (incl B) * the ObjectMap of (incl D)) ** the MorphMap of (incl D)) . i by A7, A10, A5, A6, PBOOLE:def_19; ::_thesis: verum
end;
then A11: the MorphMap of (incl C) = ( the MorphMap of (incl B) * the ObjectMap of (incl D)) ** the MorphMap of (incl D) by A1, PBOOLE:3;
the ObjectMap of (incl C) = id [: the carrier of D, the carrier of D:] by A1, FUNCTOR0:def_28
.= id ([: the carrier of B, the carrier of B:] /\ [: the carrier of D, the carrier of D:]) by A2, XBOOLE_1:28, ZFMISC_1:96
.= (id [: the carrier of B, the carrier of B:]) * (id [: the carrier of D, the carrier of D:]) by FUNCT_1:22
.= (id [: the carrier of B, the carrier of B:]) * the ObjectMap of (incl D) by FUNCTOR0:def_28
.= the ObjectMap of (incl B) * the ObjectMap of (incl D) by FUNCTOR0:def_28 ;
hence  incl C = (incl B) * (incl D) by A1, A11, FUNCTOR0:def_36; ::_thesis: verum
end;

theorem Th5: :: FUNCTOR1:5
for A, B being non empty AltCatStr
for F being FunctorStr over A,B st F is bijective holds
( the ObjectMap of F is bijective & the MorphMap of F is "1-1" )
proof
let A, B be non empty AltCatStr ; ::_thesis: for F being FunctorStr over A,B st F is bijective holds
( the ObjectMap of F is bijective & the MorphMap of F is "1-1" )
let F be FunctorStr over A,B; ::_thesis: ( F is bijective implies ( the ObjectMap of F is bijective & the MorphMap of F is "1-1" ) )
assume A1: F is bijective ; ::_thesis: ( the ObjectMap of F is bijective & the MorphMap of F is "1-1" )
then A2: F is injective by FUNCTOR0:def_35;
then  F is one-to-one by FUNCTOR0:def_33;
then A3: the ObjectMap of F is one-to-one by FUNCTOR0:def_6;
 F is surjective by A1, FUNCTOR0:def_35;
then  F is onto by FUNCTOR0:def_34;
then A4: the ObjectMap of F is onto by FUNCTOR0:def_7;
 F is faithful by A2, FUNCTOR0:def_33;
hence  ( the ObjectMap of F is bijective & the MorphMap of F is "1-1" ) by A3, A4, FUNCTOR0:def_30; ::_thesis: verum
end;

theorem Th6: :: FUNCTOR1:6
for C1 being non empty AltGraph
for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3 st F is one-to-one & G is one-to-one holds
G * F is one-to-one
proof
let C1 be non empty AltGraph ; ::_thesis: for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3 st F is one-to-one & G is one-to-one holds
G * F is one-to-one
let C2, C3 be non empty reflexive AltGraph ; ::_thesis: for F being feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3 st F is one-to-one & G is one-to-one holds
G * F is one-to-one
let F be feasible FunctorStr over C1,C2; ::_thesis: for G being FunctorStr over C2,C3 st F is one-to-one & G is one-to-one holds
G * F is one-to-one
let G be FunctorStr over C2,C3; ::_thesis: ( F is one-to-one & G is one-to-one implies G * F is one-to-one )
assume  ( F is one-to-one & G is one-to-one ) ; ::_thesis: G * F is one-to-one
then A1: ( the ObjectMap of F is one-to-one & the ObjectMap of G is one-to-one ) by FUNCTOR0:def_6;
 the ObjectMap of (G * F) = the ObjectMap of G * the ObjectMap of F by FUNCTOR0:def_36;
hence  the ObjectMap of (G * F) is one-to-one by A1; :: according to FUNCTOR0:def_6 ::_thesis: verum
end;

theorem Th7: :: FUNCTOR1:7
for C1 being non empty AltGraph
for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3 st F is faithful & G is faithful holds
G * F is faithful
proof
let C1 be non empty AltGraph ; ::_thesis: for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3 st F is faithful & G is faithful holds
G * F is faithful
let C2, C3 be non empty reflexive AltGraph ; ::_thesis: for F being feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3 st F is faithful & G is faithful holds
G * F is faithful
let F be feasible FunctorStr over C1,C2; ::_thesis: for G being FunctorStr over C2,C3 st F is faithful & G is faithful holds
G * F is faithful
let G be FunctorStr over C2,C3; ::_thesis: ( F is faithful & G is faithful implies G * F is faithful )
assume that
A1: F is faithful and
A2: G is faithful ; ::_thesis: G * F is faithful
set MMG = the MorphMap of G;
A3: the MorphMap of G is "1-1" by A2, FUNCTOR0:def_30;
set MMF = the MorphMap of F;
set CC2 = [: the carrier of C2, the carrier of C2:];
set CC1 = [: the carrier of C1, the carrier of C1:];
reconsider MMGF = the MorphMap of (G * F) as ManySortedFunction of [: the carrier of C1, the carrier of C1:] ;
reconsider OMF = the ObjectMap of F as Function of [: the carrier of C1, the carrier of C1:],[: the carrier of C2, the carrier of C2:] ;
A4: MMGF = ( the MorphMap of G * OMF) ** the MorphMap of F by FUNCTOR0:def_36;
A5: the MorphMap of F is "1-1" by A1, FUNCTOR0:def_30;
 for i being set st i in [: the carrier of C1, the carrier of C1:] holds
MMGF . i is one-to-one
proof
let i be set ; ::_thesis: ( i in [: the carrier of C1, the carrier of C1:] implies MMGF . i is one-to-one )
assume A6: i in [: the carrier of C1, the carrier of C1:] ; ::_thesis: MMGF . i is one-to-one
then  i in dom (( the MorphMap of G * OMF) ** the MorphMap of F) by PARTFUN1:def_2;
then A7: MMGF . i = (( the MorphMap of G * OMF) . i) * ( the MorphMap of F . i) by A4, PBOOLE:def_19
.= ( the MorphMap of G . (OMF . i)) * ( the MorphMap of F . i) by A6, FUNCT_2:15 ;
 OMF . i in [: the carrier of C2, the carrier of C2:] by A6, FUNCT_2:5;
then A8: the MorphMap of G . (OMF . i) is one-to-one by A3, MSUALG_3:1;
 the MorphMap of F . i is one-to-one by A5, A6, MSUALG_3:1;
hence  MMGF . i is one-to-one by A7, A8; ::_thesis: verum
end;
hence  the MorphMap of (G * F) is "1-1" by MSUALG_3:1; :: according to FUNCTOR0:def_30 ::_thesis: verum
end;

theorem Th8: :: FUNCTOR1:8
for C1 being non empty AltGraph
for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3 st F is onto & G is onto holds
G * F is onto
proof
let C1 be non empty AltGraph ; ::_thesis: for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3 st F is onto & G is onto holds
G * F is onto
let C2, C3 be non empty reflexive AltGraph ; ::_thesis: for F being feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3 st F is onto & G is onto holds
G * F is onto
let F be feasible FunctorStr over C1,C2; ::_thesis: for G being FunctorStr over C2,C3 st F is onto & G is onto holds
G * F is onto
let G be FunctorStr over C2,C3; ::_thesis: ( F is onto & G is onto implies G * F is onto )
assume that
A1: F is onto and
A2: G is onto ; ::_thesis: G * F is onto
set CC3 = [: the carrier of C3, the carrier of C3:];
set CC2 = [: the carrier of C2, the carrier of C2:];
reconsider OMG = the ObjectMap of G as Function of [: the carrier of C2, the carrier of C2:],[: the carrier of C3, the carrier of C3:] ;
 OMG is onto by A2, FUNCTOR0:def_7;
then A3: rng OMG = [: the carrier of C3, the carrier of C3:] by FUNCT_2:def_3;
set CC1 = [: the carrier of C1, the carrier of C1:];
reconsider OMF = the ObjectMap of F as Function of [: the carrier of C1, the carrier of C1:],[: the carrier of C2, the carrier of C2:] ;
 OMF is onto by A1, FUNCTOR0:def_7;
then  rng OMF = [: the carrier of C2, the carrier of C2:] by FUNCT_2:def_3;
then  rng (OMG * OMF) = [: the carrier of C3, the carrier of C3:] by A3, FUNCT_2:14;
then  OMG * OMF is onto by FUNCT_2:def_3;
hence  the ObjectMap of (G * F) is onto by FUNCTOR0:def_36; :: according to FUNCTOR0:def_7 ::_thesis: verum
end;

theorem Th9: :: FUNCTOR1:9
for C1 being non empty AltGraph
for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3 st F is full & G is full holds
G * F is full
proof
let C1 be non empty AltGraph ; ::_thesis: for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3 st F is full & G is full holds
G * F is full
let C2, C3 be non empty reflexive AltGraph ; ::_thesis: for F being feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3 st F is full & G is full holds
G * F is full
let F be feasible FunctorStr over C1,C2; ::_thesis: for G being FunctorStr over C2,C3 st F is full & G is full holds
G * F is full
let G be FunctorStr over C2,C3; ::_thesis: ( F is full & G is full implies G * F is full )
assume that
A1: F is full and
A2: G is full ; ::_thesis: G * F is full
set CC3 = [: the carrier of C3, the carrier of C3:];
set CC2 = [: the carrier of C2, the carrier of C2:];
set CC1 = [: the carrier of C1, the carrier of C1:];
reconsider OMF = the ObjectMap of F as Function of [: the carrier of C1, the carrier of C1:],[: the carrier of C2, the carrier of C2:] ;
reconsider OMG = the ObjectMap of G as Function of [: the carrier of C2, the carrier of C2:],[: the carrier of C3, the carrier of C3:] ;
consider MMF being ManySortedFunction of the Arrows of C1, the Arrows of C2 * the ObjectMap of F such that
A3: MMF = the MorphMap of F and
A4: MMF is "onto" by A1, FUNCTOR0:def_32;
consider MMG being ManySortedFunction of the Arrows of C2, the Arrows of C3 * the ObjectMap of G such that
A5: MMG = the MorphMap of G and
A6: MMG is "onto" by A2, FUNCTOR0:def_32;
 ex f being ManySortedFunction of the Arrows of C1, the Arrows of C3 * the ObjectMap of (G * F) st
( f = the MorphMap of (G * F) & f is "onto" )
proof
reconsider MMGF = the MorphMap of (G * F) as ManySortedFunction of the Arrows of C1, the Arrows of C3 * the ObjectMap of (G * F) by FUNCTOR0:def_4;
take  MMGF ; ::_thesis: ( MMGF = the MorphMap of (G * F) & MMGF is "onto" )
A7: MMGF = (MMG * OMF) ** MMF by A3, A5, FUNCTOR0:def_36;
 for i being set st i in [: the carrier of C1, the carrier of C1:] holds
rng (MMGF . i) = ( the Arrows of C3 * the ObjectMap of (G * F)) . i
proof
let i be set ; ::_thesis: ( i in [: the carrier of C1, the carrier of C1:] implies rng (MMGF . i) = ( the Arrows of C3 * the ObjectMap of (G * F)) . i )
assume A8: i in [: the carrier of C1, the carrier of C1:] ; ::_thesis: rng (MMGF . i) = ( the Arrows of C3 * the ObjectMap of (G * F)) . i
then reconsider MMGI = MMG . (OMF . i) as Function of ( the Arrows of C2 . (OMF . i)),(( the Arrows of C3 * the ObjectMap of G) . (OMF . i)) by FUNCT_2:5, PBOOLE:def_15;
A9: OMF . i in [: the carrier of C2, the carrier of C2:] by A8, FUNCT_2:5;
A10: rng ((MMG . (OMF . i)) * (MMF . i)) = rng (MMG . (OMF . i))
proof
percases ( rng MMGI = {} or rng MMGI <> {} ) ;
supposeA11: rng MMGI = {} ; ::_thesis: rng ((MMG . (OMF . i)) * (MMF . i)) = rng (MMG . (OMF . i))
 rng ({} * (MMF . i)) = {} ;
hence  rng ((MMG . (OMF . i)) * (MMF . i)) = rng (MMG . (OMF . i)) by A11, RELAT_1:41; ::_thesis: verum
end;
supposeA12: rng MMGI <> {} ; ::_thesis: rng ((MMG . (OMF . i)) * (MMF . i)) = rng (MMG . (OMF . i))
 rng MMGI = ( the Arrows of C3 * the ObjectMap of G) . (OMF . i) by A6, A9, MSUALG_3:def_3;
then  dom MMGI = the Arrows of C2 . (OMF . i) by A12, FUNCT_2:def_1;
then  dom MMGI = ( the Arrows of C2 * OMF) . i by A8, FUNCT_2:15
.= rng (MMF . i) by A4, A8, MSUALG_3:def_3 ;
hence  rng ((MMG . (OMF . i)) * (MMF . i)) = rng (MMG . (OMF . i)) by RELAT_1:28; ::_thesis: verum
end;
end;
end;
 i in dom ((MMG * OMF) ** MMF) by A8, PARTFUN1:def_2;
then  rng (MMGF . i) = rng (((MMG * OMF) . i) * (MMF . i)) by A7, PBOOLE:def_19
.= rng (MMG . (OMF . i)) by A8, A10, FUNCT_2:15
.= ( the Arrows of C3 * the ObjectMap of G) . (OMF . i) by A6, A9, MSUALG_3:def_3
.= the Arrows of C3 . (OMG . (OMF . i)) by A8, FUNCT_2:5, FUNCT_2:15
.= the Arrows of C3 . ((OMG * OMF) . i) by A8, FUNCT_2:15
.= the Arrows of C3 . ( the ObjectMap of (G * F) . i) by FUNCTOR0:def_36
.= ( the Arrows of C3 * the ObjectMap of (G * F)) . i by A8, FUNCT_2:15 ;
hence  rng (MMGF . i) = ( the Arrows of C3 * the ObjectMap of (G * F)) . i ; ::_thesis: verum
end;
hence  ( MMGF = the MorphMap of (G * F) & MMGF is "onto" ) by MSUALG_3:def_3; ::_thesis: verum
end;
hence  G * F is full by FUNCTOR0:def_32; ::_thesis: verum
end;

theorem Th10: :: FUNCTOR1:10
for C1 being non empty AltGraph
for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3 st F is injective & G is injective holds
G * F is injective
proof
let C1 be non empty AltGraph ; ::_thesis: for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3 st F is injective & G is injective holds
G * F is injective
let C2, C3 be non empty reflexive AltGraph ; ::_thesis: for F being feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3 st F is injective & G is injective holds
G * F is injective
let F be feasible FunctorStr over C1,C2; ::_thesis: for G being FunctorStr over C2,C3 st F is injective & G is injective holds
G * F is injective
let G be FunctorStr over C2,C3; ::_thesis: ( F is injective & G is injective implies G * F is injective )
assume A1: ( F is injective & G is injective ) ; ::_thesis: G * F is injective
then  ( F is faithful & G is faithful ) by FUNCTOR0:def_33;
then A2: G * F is faithful by Th7;
 ( F is one-to-one & G is one-to-one ) by A1, FUNCTOR0:def_33;
then  G * F is one-to-one by Th6;
hence  G * F is injective by A2, FUNCTOR0:def_33; ::_thesis: verum
end;

theorem Th11: :: FUNCTOR1:11
for C1 being non empty AltGraph
for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3 st F is surjective & G is surjective holds
G * F is surjective
proof
let C1 be non empty AltGraph ; ::_thesis: for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3 st F is surjective & G is surjective holds
G * F is surjective
let C2, C3 be non empty reflexive AltGraph ; ::_thesis: for F being feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3 st F is surjective & G is surjective holds
G * F is surjective
let F be feasible FunctorStr over C1,C2; ::_thesis: for G being FunctorStr over C2,C3 st F is surjective & G is surjective holds
G * F is surjective
let G be FunctorStr over C2,C3; ::_thesis: ( F is surjective & G is surjective implies G * F is surjective )
assume A1: ( F is surjective & G is surjective ) ; ::_thesis: G * F is surjective
then  ( F is onto & G is onto ) by FUNCTOR0:def_34;
then A2: G * F is onto by Th8;
 ( F is full & G is full ) by A1, FUNCTOR0:def_34;
then  G * F is full by Th9;
hence  G * F is surjective by A2, FUNCTOR0:def_34; ::_thesis: verum
end;

theorem Th12: :: FUNCTOR1:12
for C1 being non empty AltGraph
for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3 st F is bijective & G is bijective holds
G * F is bijective
proof
let C1 be non empty AltGraph ; ::_thesis: for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3 st F is bijective & G is bijective holds
G * F is bijective
let C2, C3 be non empty reflexive AltGraph ; ::_thesis: for F being feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3 st F is bijective & G is bijective holds
G * F is bijective
let F be feasible FunctorStr over C1,C2; ::_thesis: for G being FunctorStr over C2,C3 st F is bijective & G is bijective holds
G * F is bijective
let G be FunctorStr over C2,C3; ::_thesis: ( F is bijective & G is bijective implies G * F is bijective )
assume A1: ( F is bijective & G is bijective ) ; ::_thesis: G * F is bijective
then  ( F is surjective & G is surjective ) by FUNCTOR0:def_35;
then A2: G * F is surjective by Th11;
 ( F is injective & G is injective ) by A1, FUNCTOR0:def_35;
then  G * F is injective by Th10;
hence  G * F is bijective by A2, FUNCTOR0:def_35; ::_thesis: verum
end;

begin

theorem :: FUNCTOR1:13
for A, I being non empty reflexive AltCatStr
for B being non empty reflexive SubCatStr of A
for C being non empty SubCatStr of A
for D being non empty SubCatStr of B st C = D holds
for F being FunctorStr over A,I holds F | C = (F | B) | D
proof
let A, I be non empty reflexive AltCatStr ; ::_thesis: for B being non empty reflexive SubCatStr of A
for C being non empty SubCatStr of A
for D being non empty SubCatStr of B st C = D holds
for F being FunctorStr over A,I holds F | C = (F | B) | D
let B be non empty reflexive SubCatStr of A; ::_thesis: for C being non empty SubCatStr of A
for D being non empty SubCatStr of B st C = D holds
for F being FunctorStr over A,I holds F | C = (F | B) | D
let C be non empty SubCatStr of A; ::_thesis: for D being non empty SubCatStr of B st C = D holds
for F being FunctorStr over A,I holds F | C = (F | B) | D
let D be non empty SubCatStr of B; ::_thesis: ( C = D implies for F being FunctorStr over A,I holds F | C = (F | B) | D )
assume A1: C = D ; ::_thesis: for F being FunctorStr over A,I holds F | C = (F | B) | D
let F be FunctorStr over A,I; ::_thesis: F | C = (F | B) | D
thus F | C = F * ((incl B) * (incl D)) by A1, Th4
.= (F | B) | D by FUNCTOR0:32 ; ::_thesis: verum
end;

theorem :: FUNCTOR1:14
for A being non empty AltCatStr
for B being non empty SubCatStr of A holds
( B is full iff incl B is full )
proof
let A be non empty AltCatStr ; ::_thesis: for B being non empty SubCatStr of A holds
( B is full iff incl B is full )
let B be non empty SubCatStr of A; ::_thesis: ( B is full iff incl B is full )
hereby  ::_thesis: ( incl B is full implies B is full )
 ex I29 being non empty set ex B9 being ManySortedSet of I29 ex f9 being Function of [: the carrier of B, the carrier of B:],I29 st
( the ObjectMap of (incl B) = f9 & the Arrows of A = B9 & the MorphMap of (incl B) is ManySortedFunction of the Arrows of B,B9 * f9 ) by FUNCTOR0:def_3;
then reconsider f = the MorphMap of (incl B) as ManySortedFunction of the Arrows of B, the Arrows of A * the ObjectMap of (incl B) ;
set I = [: the carrier of B, the carrier of B:];
 ( the carrier of B c= the carrier of A & dom the Arrows of A = [: the carrier of A, the carrier of A:] ) by ALTCAT_2:def_11, PARTFUN1:def_2;
then A1: (dom the Arrows of A) /\ [: the carrier of B, the carrier of B:] = [: the carrier of B, the carrier of B:] by XBOOLE_1:28, ZFMISC_1:96;
assume A2: B is full ; ::_thesis: incl B is full
 f is "onto"
proof
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 (incl B)) . i )
assume A3: i in [: the carrier of B, the carrier of B:] ; ::_thesis: rng (f . i) = ( the Arrows of A * the ObjectMap of (incl B)) . i
 the Arrows of B = the Arrows of A || the carrier of B by A2, ALTCAT_2:def_13;
then A4: the Arrows of B . i = the Arrows of A . i by A3, FUNCT_1:49;
rng (f . i) = rng ((id the Arrows of B) . i) by FUNCTOR0:def_28
.= rng (id ( the Arrows of B . i)) by A3, MSUALG_3:def_1
.= the Arrows of A . i by A4
.= ( the Arrows of A * (id [: the carrier of B, the carrier of B:])) . i by A1, A3, FUNCT_1:20
.= ( the Arrows of A * the ObjectMap of (incl B)) . i by FUNCTOR0:def_28 ;
hence  rng (f . i) = ( the Arrows of A * the ObjectMap of (incl B)) . i ; ::_thesis: verum
end;
hence  incl B is full by FUNCTOR0:def_32; ::_thesis: verum
end;
set I = [: the carrier of B, the carrier of B:];
A5: the carrier of B c= the carrier of A by ALTCAT_2:def_11;
then A6: [: the carrier of B, the carrier of B:] c= [: the carrier of A, the carrier of A:] by ZFMISC_1:96;
 dom the Arrows of A = [: the carrier of A, the carrier of A:] by PARTFUN1:def_2;
then A7: (dom the Arrows of A) /\ [: the carrier of B, the carrier of B:] = [: the carrier of B, the carrier of B:] by A5, XBOOLE_1:28, ZFMISC_1:96;
then  dom ( the Arrows of A | [: the carrier of B, the carrier of B:]) = [: the carrier of B, the carrier of B:] by RELAT_1:61;
then reconsider XX = the Arrows of A || the carrier of B as ManySortedSet of [: the carrier of B, the carrier of B:] by PARTFUN1:def_2;
assume A8: incl B is full ; ::_thesis: B is full
A9: XX c= the Arrows of B
proof
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in [: the carrier of B, the carrier of B:] or XX . i c= the Arrows of B . i )
assume A10: i in [: the carrier of B, the carrier of B:] ; ::_thesis: XX . i c= the Arrows of B . i
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in XX . i or x in the Arrows of B . i )
assume A11: x in XX . i ; ::_thesis: x in the Arrows of B . i
 x in the Arrows of B . i
proof
consider f being ManySortedFunction of the Arrows of B, the Arrows of A * the ObjectMap of (incl B) such that
A12: f = the MorphMap of (incl B) and
A13: f is "onto" by A8, FUNCTOR0:def_32;
 f = id the Arrows of B by A12, FUNCTOR0:def_28;
then A14: rng ((id the Arrows of B) . i) = ( the Arrows of A * the ObjectMap of (incl B)) . i by A10, A13, MSUALG_3:def_3
.= ( the Arrows of A * (id [: the carrier of B, the carrier of B:])) . i by FUNCTOR0:def_28
.= the Arrows of A . i by A7, A10, FUNCT_1:20 ;
consider y, z being set  such that
 y in the carrier of A and
 z in the carrier of A and
A15: i = [y,z] by A6, A10, ZFMISC_1:84;
 ( y in the carrier of B & z in the carrier of B ) by A10, A15, ZFMISC_1:87;
then A16: XX . (y,z) = the Arrows of A . (y,z) by A5, ALTCAT_1:5;
rng ((id the Arrows of B) . i) = rng (id ( the Arrows of B . i)) by A10, MSUALG_3:def_1
.= the Arrows of B . i ;
hence  x in the Arrows of B . i by A11, A15, A16, A14; ::_thesis: verum
end;
hence  x in the Arrows of B . i ; ::_thesis: verum
end;
 the Arrows of B c= XX
proof
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in [: the carrier of B, the carrier of B:] or the Arrows of B . i c= XX . i )
assume A17: i in [: the carrier of B, the carrier of B:] ; ::_thesis: the Arrows of B . i c= XX . i
then consider y, z being set  such that
 y in the carrier of A and
 z in the carrier of A and
A18: i = [y,z] by A6, ZFMISC_1:84;
 ( y in the carrier of B & z in the carrier of B ) by A17, A18, ZFMISC_1:87;
then A19: XX . (y,z) = the Arrows of A . (y,z) by A5, ALTCAT_1:5;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the Arrows of B . i or x in XX . i )
assume A20: x in the Arrows of B . i ; ::_thesis: x in XX . i
 the Arrows of B cc= the Arrows of A by ALTCAT_2:def_11;
then  the Arrows of B . (y,z) c= the Arrows of A . (y,z) by A17, A18, ALTCAT_2:def_2;
hence  x in XX . i by A18, A20, A19; ::_thesis: verum
end;
hence  the Arrows of B = the Arrows of A || the carrier of B by A9, PBOOLE:146; :: according to ALTCAT_2:def_13 ::_thesis: verum
end;

begin

theorem :: FUNCTOR1:15
for C1, C2 being non empty AltCatStr
for F being Covariant FunctorStr over C1,C2 holds
( F is full iff for o1, o2 being object of C1 holds Morph-Map (F,o1,o2) is onto )
proof
let C1, C2 be non empty AltCatStr ; ::_thesis: for F being Covariant FunctorStr over C1,C2 holds
( F is full iff for o1, o2 being object of C1 holds Morph-Map (F,o1,o2) is onto )
let F be Covariant FunctorStr over C1,C2; ::_thesis: ( F is full iff for o1, o2 being object of C1 holds Morph-Map (F,o1,o2) is onto )
set I = [: the carrier of C1, the carrier of C1:];
hereby  ::_thesis: ( ( for o1, o2 being object of C1 holds Morph-Map (F,o1,o2) is onto ) implies F is full )
assume  F is full ; ::_thesis: for o1, o2 being object of C1 holds Morph-Map (F,o1,o2) is onto
then consider f being ManySortedFunction of the Arrows of C1, the Arrows of C2 * the ObjectMap of F such that
A1: f = the MorphMap of F and
A2: f is "onto" by FUNCTOR0:def_32;
let o1, o2 be object of C1; ::_thesis: Morph-Map (F,o1,o2) is onto
A3: [o1,o2] in [: the carrier of C1, the carrier of C1:] by ZFMISC_1:87;
then A4: [o1,o2] in dom the ObjectMap of F by FUNCT_2:def_1;
 rng (f . [o1,o2]) = ( the Arrows of C2 * the ObjectMap of F) . [o1,o2] by A2, A3, MSUALG_3:def_3;
then  rng (Morph-Map (F,o1,o2)) = the Arrows of C2 . ( the ObjectMap of F . (o1,o2)) by A1, A4, FUNCT_1:13
.= the Arrows of C2 . ((F . o1),(F . o2)) by FUNCTOR0:22
.= <^(F . o1),(F . o2)^> by ALTCAT_1:def_1 ;
hence  Morph-Map (F,o1,o2) is onto by FUNCT_2:def_3; ::_thesis: verum
end;
 ex I29 being non empty set ex B9 being ManySortedSet of I29 ex f9 being Function of [: the carrier of C1, the carrier of C1:],I29 st
( the ObjectMap of F = f9 & the Arrows of C2 = B9 & the MorphMap of F is ManySortedFunction of the Arrows of C1,B9 * f9 ) by FUNCTOR0:def_3;
then reconsider f = the MorphMap of F as ManySortedFunction of the Arrows of C1, the Arrows of C2 * the ObjectMap of F ;
assume A5: for o1, o2 being object of C1 holds Morph-Map (F,o1,o2) is onto ; ::_thesis: F is full
 f is "onto"
proof
let i be set ; :: according to MSUALG_3:def_3 ::_thesis: ( not i in [: the carrier of C1, the carrier of C1:] or rng (f . i) = ( the Arrows of C2 * the ObjectMap of F) . i )
assume  i in [: the carrier of C1, the carrier of C1:] ; ::_thesis: rng (f . i) = ( the Arrows of C2 * the ObjectMap of F) . i
then consider o1, o2 being set  such that
A6: ( o1 in the carrier of C1 & o2 in the carrier of C1 ) and
A7: i = [o1,o2] by ZFMISC_1:84;
reconsider o1 = o1, o2 = o2 as object of C1 by A6;
 [o1,o2] in [: the carrier of C1, the carrier of C1:] by ZFMISC_1:87;
then A8: [o1,o2] in dom the ObjectMap of F by FUNCT_2:def_1;
 Morph-Map (F,o1,o2) is onto by A5;
then  rng (Morph-Map (F,o1,o2)) = <^(F . o1),(F . o2)^> by FUNCT_2:def_3
.= the Arrows of C2 . ((F . o1),(F . o2)) by ALTCAT_1:def_1
.= the Arrows of C2 . ( the ObjectMap of F . (o1,o2)) by FUNCTOR0:22
.= ( the Arrows of C2 * the ObjectMap of F) . (o1,o2) by A8, FUNCT_1:13 ;
hence  rng (f . i) = ( the Arrows of C2 * the ObjectMap of F) . i by A7; ::_thesis: verum
end;
hence  ex f being ManySortedFunction of the Arrows of C1, the Arrows of C2 * the ObjectMap of F st
( f = the MorphMap of F & f is "onto" ) ; :: according to FUNCTOR0:def_32 ::_thesis: verum
end;

theorem :: FUNCTOR1:16
for C1, C2 being non empty AltCatStr
for F being Covariant FunctorStr over C1,C2 holds
( F is faithful iff for o1, o2 being object of C1 holds Morph-Map (F,o1,o2) is one-to-one )
proof
let C1, C2 be non empty AltCatStr ; ::_thesis: for F being Covariant FunctorStr over C1,C2 holds
( F is faithful iff for o1, o2 being object of C1 holds Morph-Map (F,o1,o2) is one-to-one )
let F be Covariant FunctorStr over C1,C2; ::_thesis: ( F is faithful iff for o1, o2 being object of C1 holds Morph-Map (F,o1,o2) is one-to-one )
set I = [: the carrier of C1, the carrier of C1:];
hereby  ::_thesis: ( ( for o1, o2 being object of C1 holds Morph-Map (F,o1,o2) is one-to-one ) implies F is faithful )
assume  F is faithful ; ::_thesis: for o1, o2 being object of C1 holds Morph-Map (F,o1,o2) is one-to-one
then A1: the MorphMap of F is "1-1" by FUNCTOR0:def_30;
let o1, o2 be object of C1; ::_thesis: Morph-Map (F,o1,o2) is one-to-one
 ( [o1,o2] in [: the carrier of C1, the carrier of C1:] & dom the MorphMap of F = [: the carrier of C1, the carrier of C1:] ) by PARTFUN1:def_2, ZFMISC_1:87;
hence  Morph-Map (F,o1,o2) is one-to-one by A1, MSUALG_3:def_2; ::_thesis: verum
end;
assume A2: for o1, o2 being object of C1 holds Morph-Map (F,o1,o2) is one-to-one ; ::_thesis: F is faithful
let i be set ; :: according to MSUALG_3:def_2,FUNCTOR0:def_30 ::_thesis: for b1 being set holds
( not i in dom the MorphMap of F or not the MorphMap of F . i = b1 or b1 is one-to-one )
let f be Function; ::_thesis: ( not i in dom the MorphMap of F or not the MorphMap of F . i = f or f is one-to-one )
assume that
A3: i in dom the MorphMap of F and
A4: the MorphMap of F . i = f ; ::_thesis: f is one-to-one
 dom the MorphMap of F = [: the carrier of C1, the carrier of C1:] by PARTFUN1:def_2;
then consider o1, o2 being set  such that
A5: ( o1 in the carrier of C1 & o2 in the carrier of C1 ) and
A6: i = [o1,o2] by A3, ZFMISC_1:84;
reconsider o1 = o1, o2 = o2 as object of C1 by A5;
 the MorphMap of F . (o1,o2) = Morph-Map (F,o1,o2) ;
hence  f is one-to-one by A2, A4, A6; ::_thesis: verum
end;

begin

theorem :: FUNCTOR1:17
for A being non empty transitive with_units AltCatStr holds (id A) " = id A
proof
let A be non empty transitive with_units AltCatStr ; ::_thesis: (id A) " = id A
set CCA = [: the carrier of A, the carrier of A:];
consider f being ManySortedFunction of the Arrows of A, the Arrows of A * the ObjectMap of (id A) such that
A1: f = the MorphMap of (id A) and
A2: the MorphMap of ((id A) ") = (f "") * ( the ObjectMap of (id A) ") by FUNCTOR0:def_38;
A3: for i being set st i in [: the carrier of A, the carrier of A:] holds
(id the Arrows of A) . i is one-to-one
proof
let i be set ; ::_thesis: ( i in [: the carrier of A, the carrier of A:] implies (id the Arrows of A) . i is one-to-one )
assume A4: i in [: the carrier of A, the carrier of A:] ; ::_thesis: (id the Arrows of A) . i is one-to-one
 id ( the Arrows of A . i) is one-to-one ;
hence  (id the Arrows of A) . i is one-to-one by A4, MSUALG_3:def_1; ::_thesis: verum
end;
 the MorphMap of (id A) = id the Arrows of A by FUNCTOR0:def_29;
then A5: the MorphMap of (id A) is "1-1" by A3, MSUALG_3:1;
 for i being set st i in [: the carrier of A, the carrier of A:] holds
rng (f . i) = ( the Arrows of A * the ObjectMap of (id A)) . i
proof
 dom the Arrows of A = [: the carrier of A, the carrier of A:] by PARTFUN1:def_2;
then A6: (dom the Arrows of A) /\ [: the carrier of A, the carrier of A:] = [: the carrier of A, the carrier of A:] ;
let i be set ; ::_thesis: ( i in [: the carrier of A, the carrier of A:] implies rng (f . i) = ( the Arrows of A * the ObjectMap of (id A)) . i )
assume A7: i in [: the carrier of A, the carrier of A:] ; ::_thesis: rng (f . i) = ( the Arrows of A * the ObjectMap of (id A)) . i
rng (f . i) = rng ((id the Arrows of A) . i) by A1, FUNCTOR0:def_29
.= rng (id ( the Arrows of A . i)) by A7, MSUALG_3:def_1
.= the Arrows of A . i
.= ( the Arrows of A * (id [: the carrier of A, the carrier of A:])) . i by A7, A6, FUNCT_1:20
.= ( the Arrows of A * the ObjectMap of (id A)) . i by FUNCTOR0:def_29 ;
hence  rng (f . i) = ( the Arrows of A * the ObjectMap of (id A)) . i ; ::_thesis: verum
end;
then A8: f is "onto" by MSUALG_3:def_3;
 for i being set st i in [: the carrier of A, the carrier of A:] holds
(f "") . i = f . i
proof
let i be set ; ::_thesis: ( i in [: the carrier of A, the carrier of A:] implies (f "") . i = f . i )
assume A9: i in [: the carrier of A, the carrier of A:] ; ::_thesis: (f "") . i = f . i
then (f "") . i = ( the MorphMap of (id A) . i) " by A1, A5, A8, MSUALG_3:def_4
.= ((id the Arrows of A) . i) " by FUNCTOR0:def_29
.= (id ( the Arrows of A . i)) " by A9, MSUALG_3:def_1
.= id ( the Arrows of A . i) by FUNCT_1:45
.= (id the Arrows of A) . i by A9, MSUALG_3:def_1
.= f . i by A1, FUNCTOR0:def_29 ;
hence  (f "") . i = f . i ; ::_thesis: verum
end;
then A10: f "" = f by PBOOLE:3;
 for i being set st i in [: the carrier of A, the carrier of A:] holds
( the MorphMap of (id A) * (id [: the carrier of A, the carrier of A:])) . i = the MorphMap of (id A) . i
proof
 dom the MorphMap of (id A) = [: the carrier of A, the carrier of A:] by PARTFUN1:def_2;
then A11: (dom the MorphMap of (id A)) /\ [: the carrier of A, the carrier of A:] = [: the carrier of A, the carrier of A:] ;
let i be set ; ::_thesis: ( i in [: the carrier of A, the carrier of A:] implies ( the MorphMap of (id A) * (id [: the carrier of A, the carrier of A:])) . i = the MorphMap of (id A) . i )
assume  i in [: the carrier of A, the carrier of A:] ; ::_thesis: ( the MorphMap of (id A) * (id [: the carrier of A, the carrier of A:])) . i = the MorphMap of (id A) . i
hence  ( the MorphMap of (id A) * (id [: the carrier of A, the carrier of A:])) . i = the MorphMap of (id A) . i by A11, FUNCT_1:20; ::_thesis: verum
end;
then A12: the MorphMap of (id A) * (id [: the carrier of A, the carrier of A:]) = the MorphMap of (id A) by PBOOLE:3;
A13: the ObjectMap of ((id A) ") = the ObjectMap of (id A) " by FUNCTOR0:def_38;
then  the ObjectMap of ((id A) ") = (id [: the carrier of A, the carrier of A:]) " by FUNCTOR0:def_29
.= id [: the carrier of A, the carrier of A:] by FUNCT_1:45
.= the ObjectMap of (id A) by FUNCTOR0:def_29 ;
hence  (id A) " = id A by A13, A1, A2, A10, A12, FUNCTOR0:def_29; ::_thesis: verum
end;

theorem :: FUNCTOR1:18
for A, B being non empty transitive with_units reflexive AltCatStr
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
proof
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, FUNCTOR0:def_35;
then  F is one-to-one by FUNCTOR0:def_33;
then A4: the ObjectMap of F is one-to-one by FUNCTOR0:def_6;
set OM = the ObjectMap of F;
 F is surjective by A1, FUNCTOR0:def_35;
then  F is onto by FUNCTOR0:def_34;
then  the ObjectMap of F is onto by FUNCTOR0:def_7;
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, FUNCTOR0:def_35;
then A6: F is faithful by FUNCTOR0:def_33;
then A7: the MorphMap of F is "1-1" by FUNCTOR0:def_30;
 F is surjective by A1, FUNCTOR0:def_35;
then  ( F is full & F is onto ) by FUNCTOR0:def_34;
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" by FUNCTOR0:def_32;
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 by FUNCTOR0:def_35;
then  ( FunctorStr(# the ObjectMap of G, the MorphMap of G #) is full & FunctorStr(# the ObjectMap of G, the MorphMap of G #) is onto ) by FUNCTOR0:def_34;
then A12: the ObjectMap of G is onto by FUNCTOR0:def_7;
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 set 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
let i be set ; ::_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, MSUALG_3:def_3
.= 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, FUNCTOR0:def_30, PARTFUN1:def_2;
then A22: f . ( the ObjectMap of G . i) is one-to-one by A19, MSUALG_3:def_2;
((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;
 the MorphMap of (F * G) = (f * the ObjectMap of G) ** ((k "") * the ObjectMap of G) by A10, A3, A8, A11, FUNCTOR0:def_36;
then A23: the MorphMap of (F * G) = id the Arrows of B by A15, PBOOLE:3;
 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
end;

Lm1:  for I being set
for A, B being ManySortedSet of I st A is_transformable_to B holds
for H being ManySortedFunction of A,B
for H1 being ManySortedFunction of B,A st H is "1-1" & H is "onto" & H1 = H "" holds
( H ** H1 = id B & H1 ** H = id A )
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I st A is_transformable_to B holds
for H being ManySortedFunction of A,B
for H1 being ManySortedFunction of B,A st H is "1-1" & H is "onto" & H1 = H "" holds
( H ** H1 = id B & H1 ** H = id A )
let A, B be ManySortedSet of I; ::_thesis: ( A is_transformable_to B implies for H being ManySortedFunction of A,B
for H1 being ManySortedFunction of B,A st H is "1-1" & H is "onto" & H1 = H "" holds
( H ** H1 = id B & H1 ** H = id A ) )
assume A1: A is_transformable_to B ; ::_thesis: for H being ManySortedFunction of A,B
for H1 being ManySortedFunction of B,A st H is "1-1" & H is "onto" & H1 = H "" holds
( H ** H1 = id B & H1 ** H = id A )
let H be ManySortedFunction of A,B; ::_thesis: for H1 being ManySortedFunction of B,A st H is "1-1" & H is "onto" & H1 = H "" holds
( H ** H1 = id B & H1 ** H = id A )
let H1 be ManySortedFunction of B,A; ::_thesis: ( H is "1-1" & H is "onto" & H1 = H "" implies ( H ** H1 = id B & H1 ** H = id A ) )
assume that
A2: ( H is "1-1" & H is "onto" ) and
A3: H1 = H "" ; ::_thesis: ( H ** H1 = id B & H1 ** H = id A )
reconsider F1 = H ** H1 as ManySortedFunction of I ;
A4: now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(H_**_H1)_._i_=_id_(B_._i)
let i be set ; ::_thesis: ( i in I implies (H ** H1) . i = id (B . i) )
assume A5: i in I ; ::_thesis: (H ** H1) . i = id (B . i)
then reconsider h = H . i as Function of (A . i),(B . i) by PBOOLE:def_15;
reconsider h1 = H1 . i as Function of (B . i),(A . i) by A5, PBOOLE:def_15;
 i in dom H by A5, PARTFUN1:def_2;
then A6: h is one-to-one by A2, MSUALG_3:def_2;
 h1 = h " by A2, A3, A5, MSUALG_3:def_4;
then  h * h1 = id (rng h) by A6, FUNCT_1:39;
then  h * h1 = id (B . i) by A2, A5, MSUALG_3:def_3;
hence  (H ** H1) . i = id (B . i) by A5, MSUALG_3:2; ::_thesis: verum
end;
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
F1_._i_is_Function_of_(B_._i),(B_._i)
let i be set ; ::_thesis: ( i in I implies F1 . i is Function of (B . i),(B . i) )
assume  i in I ; ::_thesis: F1 . i is Function of (B . i),(B . i)
then  F1 . i = id (B . i) by A4;
hence  F1 . i is Function of (B . i),(B . i) ; ::_thesis: verum
end;
then A7: F1 is ManySortedFunction of B,B by PBOOLE:def_15;
reconsider F = H1 ** H as ManySortedFunction of I ;
A8: for i being set st i in I holds
(H1 ** H) . i = id (A . i)
proof
let i be set ; ::_thesis: ( i in I implies (H1 ** H) . i = id (A . i) )
assume A9: i in I ; ::_thesis: (H1 ** H) . i = id (A . i)
then reconsider h = H . i as Function of (A . i),(B . i) by PBOOLE:def_15;
reconsider h1 = H1 . i as Function of (B . i),(A . i) by A9, PBOOLE:def_15;
 i in dom H by A9, PARTFUN1:def_2;
then A10: h is one-to-one by A2, MSUALG_3:def_2;
 ( B . i = {} implies A . i = {} ) by A1, A9, PZFMISC1:def_3;
then A11: dom h = A . i by FUNCT_2:def_1;
 h1 = h " by A2, A3, A9, MSUALG_3:def_4;
then  h1 * h = id (A . i) by A10, A11, FUNCT_1:39;
hence  (H1 ** H) . i = id (A . i) by A9, MSUALG_3:2; ::_thesis: verum
end;
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(H1_**_H)_._i_is_Function_of_(A_._i),(A_._i)
let i be set ; ::_thesis: ( i in I implies (H1 ** H) . i is Function of (A . i),(A . i) )
assume  i in I ; ::_thesis: (H1 ** H) . i is Function of (A . i),(A . i)
then  (H1 ** H) . i = id (A . i) by A8;
hence  (H1 ** H) . i is Function of (A . i),(A . i) ; ::_thesis: verum
end;
then reconsider F = F as ManySortedFunction of A,A by PBOOLE:def_15;
 F = id A by A8, MSUALG_3:def_1;
hence  ( H ** H1 = id B & H1 ** H = id A ) by A4, A7, MSUALG_3:def_1; ::_thesis: verum
end;

theorem :: FUNCTOR1:19
for A, B being non empty transitive with_units reflexive AltCatStr
for F being feasible FunctorStr over A,B st F is bijective holds
(F ") * F = id A
proof
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
proof
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 set  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;
 F is injective by A1, FUNCTOR0:def_35;
then  F is faithful by FUNCTOR0:def_33;
then A10: the MorphMap of F is "1-1" by FUNCTOR0:def_30;
 for i being set 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
let i be set ; ::_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;
then A12: (f "") * (id [: the carrier of A, the carrier of A:]) = f "" by PBOOLE:3;
 F is injective by A1, FUNCTOR0:def_35;
then  F is one-to-one by FUNCTOR0:def_33;
then A13: the ObjectMap of F is one-to-one by FUNCTOR0:def_6;
 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, FUNCTOR0:def_35;
then  ( F is full & F is onto ) by FUNCTOR0:def_34;
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" ) by FUNCTOR0:def_32;
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
end;

theorem :: FUNCTOR1:20
for A, B being non empty transitive with_units reflexive AltCatStr
for F being feasible FunctorStr over A,B st F is bijective holds
(F ") " = FunctorStr(# the ObjectMap of F, the MorphMap of F #)
proof
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, FUNCTOR0:def_35;
then  F is one-to-one by FUNCTOR0:def_33;
then A3: the ObjectMap of F is one-to-one by FUNCTOR0:def_6;
A4: F " is bijective by A1, FUNCTOR0:35;
then  F " is surjective by FUNCTOR0:def_35;
then A5: F " is full by FUNCTOR0:def_34;
 F " is injective by A4, FUNCTOR0:def_35;
then A6: F " is faithful by FUNCTOR0:def_33;
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, FUNCTOR0:def_33;
then A8: the MorphMap of F is "1-1" by FUNCTOR0:def_30;
A9: F is surjective by A1, FUNCTOR0:def_35;
then  F is onto by FUNCTOR0:def_34;
then  the ObjectMap of F is onto by FUNCTOR0:def_7;
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, FUNCTOR0:def_34;
 the MorphMap of ((F ") ") = the MorphMap of F
proof
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, FUNCTOR0:def_32;
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, FUNCTOR0:def_32;
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, FUNCTOR0:def_30;
 for i being set st i in [: the carrier of A, the carrier of A:] holds
((f "") * ( the ObjectMap of (F ") ")) . i = the MorphMap of F . i
proof
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 set ; ::_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;
hence  the MorphMap of ((F ") ") = the MorphMap of F by A15, PBOOLE:3; ::_thesis: verum
end;
hence  (F ") " = FunctorStr(# the ObjectMap of F, the MorphMap of F #) by A4, A7, FUNCTOR0:def_38; ::_thesis: verum
end;

theorem :: FUNCTOR1:21
for A, B, C being non empty transitive with_units reflexive AltCatStr
for G being feasible FunctorStr over A,B
for F being feasible FunctorStr over B,C
for GI being feasible FunctorStr over B,A
for FI being feasible FunctorStr over C,B st F is bijective & G is bijective & FunctorStr(# the ObjectMap of GI, the MorphMap of GI #) = G " & FunctorStr(# the ObjectMap of FI, the MorphMap of FI #) = F " holds
(F * G) " = GI * FI
proof
let A, B, C be non empty transitive with_units reflexive AltCatStr ; ::_thesis: for G being feasible FunctorStr over A,B
for F being feasible FunctorStr over B,C
for GI being feasible FunctorStr over B,A
for FI being feasible FunctorStr over C,B st F is bijective & G is bijective & FunctorStr(# the ObjectMap of GI, the MorphMap of GI #) = G " & FunctorStr(# the ObjectMap of FI, the MorphMap of FI #) = F " holds
(F * G) " = GI * FI
let G be feasible FunctorStr over A,B; ::_thesis: for F being feasible FunctorStr over B,C
for GI being feasible FunctorStr over B,A
for FI being feasible FunctorStr over C,B st F is bijective & G is bijective & FunctorStr(# the ObjectMap of GI, the MorphMap of GI #) = G " & FunctorStr(# the ObjectMap of FI, the MorphMap of FI #) = F " holds
(F * G) " = GI * FI
let F be feasible FunctorStr over B,C; ::_thesis: for GI being feasible FunctorStr over B,A
for FI being feasible FunctorStr over C,B st F is bijective & G is bijective & FunctorStr(# the ObjectMap of GI, the MorphMap of GI #) = G " & FunctorStr(# the ObjectMap of FI, the MorphMap of FI #) = F " holds
(F * G) " = GI * FI
let GI be feasible FunctorStr over B,A; ::_thesis: for FI being feasible FunctorStr over C,B st F is bijective & G is bijective & FunctorStr(# the ObjectMap of GI, the MorphMap of GI #) = G " & FunctorStr(# the ObjectMap of FI, the MorphMap of FI #) = F " holds
(F * G) " = GI * FI
let FI be feasible FunctorStr over C,B; ::_thesis: ( F is bijective & G is bijective & FunctorStr(# the ObjectMap of GI, the MorphMap of GI #) = G " & FunctorStr(# the ObjectMap of FI, the MorphMap of FI #) = F " implies (F * G) " = GI * FI )
assume that
A1: F is bijective and
A2: G is bijective and
A3: FunctorStr(# the ObjectMap of GI, the MorphMap of GI #) = G " and
A4: FunctorStr(# the ObjectMap of FI, the MorphMap of FI #) = F " ; ::_thesis: (F * G) " = GI * FI
reconsider MF = the MorphMap of F as ManySortedFunction of the Arrows of B, the Arrows of C * the ObjectMap of F by FUNCTOR0:def_4;
A5: MF is "1-1" by A1, Th5;
set OG = the ObjectMap of G;
set CB = [: the carrier of B, the carrier of B:];
set CA = [: the carrier of A, the carrier of A:];
reconsider OGI = the ObjectMap of G " as Function of [: the carrier of B, the carrier of B:],[: the carrier of A, the carrier of A:] by A2, Th2, Th5;
set CC = [: the carrier of C, the carrier of C:];
set OF = the ObjectMap of F;
reconsider OFI = the ObjectMap of F " as Function of [: the carrier of C, the carrier of C:],[: the carrier of B, the carrier of B:] by A1, Th2, Th5;
reconsider MFG = the MorphMap of (F * G) as ManySortedFunction of the Arrows of A, the Arrows of C * the ObjectMap of (F * G) by FUNCTOR0:def_4;
reconsider OG = the ObjectMap of G as Function of [: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:] ;
reconsider OFG = the ObjectMap of (F * G) as Function of [: the carrier of A, the carrier of A:],[: the carrier of C, the carrier of C:] ;
reconsider MG = the MorphMap of G as ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of G by FUNCTOR0:def_4;
A6: MG is "1-1" by A2, Th5;
 F is surjective by A1, FUNCTOR0:def_35;
then  F is full by FUNCTOR0:def_34;
then A7: ex mf being ManySortedFunction of the Arrows of B, the Arrows of C * the ObjectMap of F st
( mf = the MorphMap of F & mf is "onto" ) by FUNCTOR0:def_32;
 F is injective by A1, FUNCTOR0:def_35;
then  F is one-to-one by FUNCTOR0:def_33;
then A8: the ObjectMap of F is one-to-one by FUNCTOR0:def_6;
A9: G is surjective by A2, FUNCTOR0:def_35;
then  G is onto by FUNCTOR0:def_34;
then A10: the ObjectMap of G is onto by FUNCTOR0:def_7;
 G is full by A9, FUNCTOR0:def_34;
then A11: ex mg being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of G st
( mg = the MorphMap of G & mg is "onto" ) by FUNCTOR0:def_32;
 G is injective by A2, FUNCTOR0:def_35;
then  G is one-to-one by FUNCTOR0:def_33;
then A12: the ObjectMap of G is one-to-one by FUNCTOR0:def_6;
A13: F * G is bijective by A1, A2, Th12;
then  F * G is surjective by FUNCTOR0:def_35;
then  F * G is full by FUNCTOR0:def_34;
then A14: ex mfg being ManySortedFunction of the Arrows of A, the Arrows of C * the ObjectMap of (F * G) st
( mfg = the MorphMap of (F * G) & mfg is "onto" ) by FUNCTOR0:def_32;
A15: MFG is "1-1" by A13, Th5;
A16: the MorphMap of ((F * G) ") = the MorphMap of (GI * FI)
proof
consider f being ManySortedFunction of the Arrows of A, the Arrows of C * the ObjectMap of (F * G) such that
A17: f = the MorphMap of (F * G) and
A18: the MorphMap of ((F * G) ") = (f "") * ( the ObjectMap of (F * G) ") by A13, FUNCTOR0:def_38;
A19: rng the ObjectMap of G = [: the carrier of B, the carrier of B:] by A10, FUNCT_2:def_3;
 for i being set st i in [: the carrier of C, the carrier of C:] holds
((f "") * ( the ObjectMap of (F * G) ")) . i = (( the MorphMap of (G ") * the ObjectMap of (F ")) ** the MorphMap of (F ")) . i
proof
A20: ( ex x1 being ManySortedFunction of the Arrows of B, the Arrows of C * the ObjectMap of F st
( x1 = the MorphMap of F & the MorphMap of (F ") = (x1 "") * ( the ObjectMap of F ") ) & ex x1 being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of G st
( x1 = the MorphMap of G & the MorphMap of (G ") = (x1 "") * ( the ObjectMap of G ") ) ) by A1, A2, FUNCTOR0:def_38;
A21: ( the ObjectMap of F " = the ObjectMap of (F ") & dom ((((MG "") * OGI) * OFI) ** ((MF "") * OFI)) = [: the carrier of C, the carrier of C:] ) by A1, FUNCTOR0:def_38, PARTFUN1:def_2;
A22: OG * (OG ") = id [: the carrier of B, the carrier of B:] by A12, A19, FUNCT_2:29;
A23: OFG " = ( the ObjectMap of F * OG) " by FUNCTOR0:def_36
.= (OG ") * ( the ObjectMap of F ") by A8, A12, FUNCT_1:44 ;
let i be set ; ::_thesis: ( i in [: the carrier of C, the carrier of C:] implies ((f "") * ( the ObjectMap of (F * G) ")) . i = (( the MorphMap of (G ") * the ObjectMap of (F ")) ** the MorphMap of (F ")) . i )
assume A24: i in [: the carrier of C, the carrier of C:] ; ::_thesis: ((f "") * ( the ObjectMap of (F * G) ")) . i = (( the MorphMap of (G ") * the ObjectMap of (F ")) ** the MorphMap of (F ")) . i
A25: ((MF . (OG . (((OG ") * ( the ObjectMap of F ")) . i))) * (MG . ((OFG ") . i))) " = ((MF . (OG . (OGI . (OFI . i)))) * (MG . ((OFG ") . i))) " by A24, FUNCT_2:15
.= ((MF . ((OG * OGI) . (OFI . i))) * (MG . ((OFG ") . i))) " by A24, FUNCT_2:5, FUNCT_2:15
.= ((MF . (((id [: the carrier of B, the carrier of B:]) * OFI) . i)) * (MG . ((OFG ") . i))) " by A24, A22, FUNCT_2:15
.= ((MF . (( the ObjectMap of F ") . i)) * (MG . ((OGI * OFI) . i))) " by A23, FUNCT_2:17 ;
 OFG " is Function of [: the carrier of C, the carrier of C:],[: the carrier of A, the carrier of A:] by A13, Th2, Th5;
then A26: ( dom ((MF * OG) ** MG) = [: the carrier of A, the carrier of A:] & (OFG ") . i in [: the carrier of A, the carrier of A:] ) by A24, FUNCT_2:5, PARTFUN1:def_2;
A27: the ObjectMap of (F * G) " is Function of [: the carrier of C, the carrier of C:],[: the carrier of A, the carrier of A:] by A13, Th2, Th5;
then A28: ( the ObjectMap of (F * G) ") . i in [: the carrier of A, the carrier of A:] by A24, FUNCT_2:5;
 i in dom ( the ObjectMap of (F * G) ") by A24, A27, FUNCT_2:def_1;
then A29: ((f "") * ( the ObjectMap of (F * G) ")) . i = (MFG "") . (( the ObjectMap of (F * G) ") . i) by A17, FUNCT_1:13
.= (MFG . (( the ObjectMap of (F * G) ") . i)) " by A14, A15, A28, MSUALG_3:def_4
.= (((MF * OG) ** MG) . ((OFG ") . i)) " by FUNCTOR0:def_36
.= (((MF * OG) . ((OFG ") . i)) * (MG . ((OFG ") . i))) " by A26, PBOOLE:def_19
.= ((MF . (OG . (((OG ") * ( the ObjectMap of F ")) . i))) * (MG . ((OFG ") . i))) " by A24, A27, A23, FUNCT_2:5, FUNCT_2:15 ;
A30: OFI . i in [: the carrier of B, the carrier of B:] by A24, FUNCT_2:5;
then A31: MF . (OFI . i) is one-to-one by A5, MSUALG_3:1;
A32: OGI . (OFI . i) in [: the carrier of A, the carrier of A:] by A30, FUNCT_2:5;
then A33: MG . (OGI . (OFI . i)) is one-to-one by A6, MSUALG_3:1;
((MF . (( the ObjectMap of F ") . i)) * (MG . ((OGI * OFI) . i))) " = ((MF . (( the ObjectMap of F ") . i)) * (MG . (OGI . (OFI . i)))) " by A24, FUNCT_2:15
.= ((MG . (OGI . (OFI . i))) ") * ((MF . (OFI . i)) ") by A33, A31, FUNCT_1:44
.= ((MG "") . (OGI . (OFI . i))) * ((MF . (( the ObjectMap of F ") . i)) ") by A11, A6, A32, MSUALG_3:def_4
.= (((MG "") * OGI) . (OFI . i)) * ((MF . (( the ObjectMap of F ") . i)) ") by A24, FUNCT_2:5, FUNCT_2:15
.= ((((MG "") * OGI) * OFI) . i) * ((MF . (OFI . i)) ") by A24, FUNCT_2:15
.= ((((MG "") * OGI) * OFI) . i) * ((MF "") . (OFI . i)) by A5, A7, A30, MSUALG_3:def_4
.= ((((MG "") * OGI) * OFI) . i) * (((MF "") * OFI) . i) by A24, FUNCT_2:15 ;
hence  ((f "") * ( the ObjectMap of (F * G) ")) . i = (( the MorphMap of (G ") * the ObjectMap of (F ")) ** the MorphMap of (F ")) . i by A20, A24, A21, A29, A25, PBOOLE:def_19; ::_thesis: verum
end;
then  the MorphMap of ((F * G) ") = ( the MorphMap of GI * the ObjectMap of FI) ** the MorphMap of FI by A3, A4, A18, PBOOLE:3
.= the MorphMap of (GI * FI) by FUNCTOR0:def_36 ;
hence  the MorphMap of ((F * G) ") = the MorphMap of (GI * FI) ; ::_thesis: verum
end;
the ObjectMap of ((F * G) ") = the ObjectMap of (F * G) " by A13, FUNCTOR0:def_38
.= ( the ObjectMap of F * the ObjectMap of G) " by FUNCTOR0:def_36
.= ( the ObjectMap of G ") * ( the ObjectMap of F ") by A8, A12, FUNCT_1:44
.= the ObjectMap of GI * ( the ObjectMap of F ") by A2, A3, FUNCTOR0:def_38
.= the ObjectMap of GI * the ObjectMap of FI by A1, A4, FUNCTOR0:def_38
.= the ObjectMap of (GI * FI) by FUNCTOR0:def_36 ;
hence  (F * G) " = GI * FI by A16; ::_thesis: verum
end;