:: Functors for Alternative Categories
::  by Andrzej Trybulec
::
:: Received April 24, 1996
:: Copyright (c) 1996-2019 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies XBOOLE_0, FUNCT_1, SUBSET_1, MCART_1, ZFMISC_1, TARSKI, PBOOLE,
      RELAT_1, FUNCT_2, FUNCOP_1, MEMBER_1, STRUCT_0, ALTCAT_1, RELAT_2,
      MSUALG_6, CAT_1, ALTCAT_2, FUNCT_3, MSUALG_3, ENS_1, WELLORD1, FUNCTOR0;
 notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, RELAT_1, MCART_1,
      FUNCT_1, PBOOLE, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1, FUNCT_3,
      FUNCT_4, STRUCT_0, MSUALG_3, ALTCAT_1, ALTCAT_2;
 constructors FUNCT_3, MSUALG_3, ALTCAT_2, RELSET_1, XTUPLE_0;
 registrations SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, PBOOLE, STRUCT_0,
      ALTCAT_1, ALTCAT_2, PARTFUN1, RELSET_1, FUNCT_3, XTUPLE_0, FUNCT_4;
 requirements SUBSET, BOOLE;
 definitions TARSKI, MSUALG_3, FUNCT_1, FUNCT_2, XBOOLE_0, PBOOLE;
 equalities XBOOLE_0, BINOP_1;
 expansions MSUALG_3, FUNCT_1, FUNCT_2, XBOOLE_0;
 theorems ALTCAT_2, FUNCT_4, FUNCOP_1, ZFMISC_1, ALTCAT_1, FUNCT_2, FUNCT_1,
      PBOOLE, FUNCT_3, RELAT_1, MCART_1, DOMAIN_1, MSUALG_3, RELSET_1,
      XBOOLE_0, XBOOLE_1, PARTFUN1, XTUPLE_0;
 schemes ALTCAT_2;

begin :: Preliminaries

scheme ValOnPair {X()-> non empty set,f()-> Function,
  x1,x2()-> Element of X(), F(object,object)-> set, P[object,object]}:
  f().(x1(),x2()) = F(x1(),x2())
provided
A1: f() = { [[o,o9],F(o,o9)]
where o is Element of X(), o9 is Element of X(): P[o,o9] } and
A2: P[x1(),x2()]
proof
  defpred R[set] means P[ $1`1,$1`2];
  deffunc G(set) = F($1`1,$1`2);
A3: f() = { [o,G(o)] where o is Element of [:X(),X():]: R[o] }
  proof
    thus
    f() c= {[o,F(o`1,o`2)] where o is Element of [:X(),X():]: P[o`1,o`2]}
    proof
      let y be object;
      assume y in f();
      then consider o1,o2 being Element of X() such that
A4:   y = [[o1,o2],F(o1,o2)] and
A5:   P[o1,o2] by A1;
      reconsider p =[o1,o2] as Element of [:X(),X():] by ZFMISC_1:87;
A6:   p`1 = o1;
      p`2 = o2;
      hence thesis by A4,A5,A6;
    end;
    let y be object;
    assume y in {[o,F(o`1,o`2)] where o is Element of [:X(),X():]: P[o`1,o`2]};
    then consider o being Element of [:X(),X():] such that
A7: y = [o,F(o`1,o`2)] and
A8: P[o`1,o`2];
    reconsider o1 = o`1, o2 = o`2 as Element of X() by MCART_1:10;
    o = [o1,o2] by MCART_1:21;
    hence thesis by A1,A7,A8;
  end;
  reconsider x = [x1(),x2()] as Element of [:X(),X():] by ZFMISC_1:87;
A9: R[ x] by A2;
  thus f().(x1(),x2()) = f().x .= G(x) from ALTCAT_2:sch 3(A3,A9)
    .= F(x1(),x2());
end;

theorem Th1:
  for A being set holds {} is Function of A,{} by FUNCT_2:130;

theorem Th2:
  for I being set for M being ManySortedSet of I holds M*id I = M
proof
  let I be set;
  let M be ManySortedSet of I;
  I = dom M by PARTFUN1:def 2;
  hence thesis by RELAT_1:52;
end;

registration
  let f be empty Function;
  cluster ~f -> empty;
  coherence;
  let g be Function;
  cluster [:f,g:] -> empty;
  coherence
  proof dom f = {};
    then dom[:f,g:] = [:{},dom g:] by FUNCT_3:def 8;
    hence thesis;
  end;
  cluster [:g,f:] -> empty;
  coherence
  proof dom f = {};
    then dom[:g,f:] = [:dom g,{}:] by FUNCT_3:def 8;
    hence thesis;
  end;
end;

theorem Th3:
  for A being set, f being Function holds f.:id A = (~f).:id A
proof
  let A be set, f be Function;
  thus f.:id A c= (~f).:id A
  proof
    let y be object;
    assume y in f.:id A;
    then consider x being object such that
A1: x in dom f and
A2: x in id A and
A3: y = f.x by FUNCT_1:def 6;
    consider x1,x2 being object such that
A4: x = [x1,x2] by A2,RELAT_1:def 1;
A5: x1 = x2 by A2,A4,RELAT_1:def 10;
    then
A6: x in dom~f by A1,A4,FUNCT_4:42;
    then f.(x1,x2) = (~f).(x1,x2) by A4,A5,FUNCT_4:43;
    hence thesis by A2,A3,A4,A6,FUNCT_1:def 6;
  end;
  let y be object;
  assume y in (~f).:id A;
  then consider x being object such that
A7: x in dom~f and
A8: x in id A and
A9: y = (~f).x by FUNCT_1:def 6;
  consider x1,x2 being object such that
A10: x = [x1,x2] by A8,RELAT_1:def 1;
A11: x1 = x2 by A8,A10,RELAT_1:def 10;
  then
A12: x in dom f by A7,A10,FUNCT_4:42;
  then ~f.(x1,x2) = f.(x1,x2) by A10,A11,FUNCT_4:def 2;
  hence thesis by A8,A9,A10,A12,FUNCT_1:def 6;
end;

theorem Th4:
  for X,Y being set, f being Function of X,Y holds
  f is onto iff [:f,f:] is onto
proof
  let X,Y be set, f be Function of X,Y;
  rng[:f,f:] = [:rng f, rng f:] by FUNCT_3:67;
  then rng f = Y iff rng[:f,f:] = [:Y,Y:] by ZFMISC_1:92;
  hence thesis;
end;

registration
  let f be Function-yielding Function;
  cluster ~f -> Function-yielding;
  coherence;
end;

theorem Th5:
  for A,B being set, a being object holds ~([:A,B:] --> a) = [:B,A:] --> a
proof
  let A,B be set, a be object;
A1: now
    let x be object;
    hereby
      assume x in dom([:B,A:] --> a);
      then consider z,y being object such that
A2:   z in B and
A3:   y in A and
A4:   x = [z,y] by ZFMISC_1:def 2;
      take y,z;
      thus x = [z,y] by A4;
      [y,z] in [:A,B:] by A2,A3,ZFMISC_1:87;
      hence [y,z] in dom([:A,B:] --> a);
    end;
    given y,z being object such that
A5: x = [z,y] and
A6: [y,z] in dom([:A,B:] --> a);
A7: y in A by A6,ZFMISC_1:87;
    z in B by A6,ZFMISC_1:87;
    then x in [:B,A:] by A5,A7,ZFMISC_1:87;
    hence x in dom([:B,A:] --> a);
  end;
  now
    let y,z be object;
    assume
A8: [y,z] in dom([:A,B:] --> a);
    then
A9: y in A by ZFMISC_1:87;
    z in B by A8,ZFMISC_1:87;
    hence ([:B,A:] --> a).(z,y) = a by A9,FUNCOP_1:7,ZFMISC_1:87
      .= ([:A,B:] --> a).(y,z) by A8,FUNCOP_1:7;
  end;
  hence thesis by A1,FUNCT_4:def 2;
end;

theorem Th6:
  for f,g being Function st f is one-to-one & g is one-to-one holds
  [:f,g:]" = [:f",g":]
proof
  let f,g be Function;
  assume that
A1: f is one-to-one and
A2: g is one-to-one;
A3: [:f,g:] is one-to-one by A1,A2;
A4: dom(f") = rng f by A1,FUNCT_1:33;
A5: dom(g") = rng g by A2,FUNCT_1:33;
A6: dom([:f,g:]") = rng[:f,g:] by A3,FUNCT_1:33
    .= [:dom(f"), dom(g"):] by A4,A5,FUNCT_3:67;
  for x,y being object st x in dom(f") & y in dom(g")
  holds [:f,g:]".(x,y) = [f".x,g".y]
  proof
    let x,y be object such that
A7: x in dom(f") and
A8: y in dom(g");
A9: dom[:f,g:] = [:dom f, dom g:] by FUNCT_3:def 8;
A10: f".x in rng(f") by A7,FUNCT_1:def 3;
A11: g".y in rng(g") by A8,FUNCT_1:def 3;
A12: f".x in dom f by A1,A10,FUNCT_1:33;
    g".y in dom g by A2,A11,FUNCT_1:33;
    then
A13: [f".x,g".y] in dom[:f,g:] by A9,A12,ZFMISC_1:87;
A14: f.(f".x) = (f*f").x by A7,FUNCT_1:13
      .= ((f")"*f").x by A1,FUNCT_1:43
      .= (id dom(f")).x by A1,FUNCT_1:39
      .= x by A7,FUNCT_1:18;
    g.(g".y) = (g*g").y by A8,FUNCT_1:13
      .= ((g")"*g").y by A2,FUNCT_1:43
      .= (id dom(g")).y by A2,FUNCT_1:39
      .= y by A8,FUNCT_1:18;
    then [:f,g:].(f".x,g".y) = [x,y] by A9,A13,A14,FUNCT_3:65;
    hence thesis by A1,A2,A13,FUNCT_1:32;
  end;
  hence thesis by A6,FUNCT_3:def 8;
end;

theorem Th7:
  for f being Function st [:f,f:] is one-to-one holds f is one-to-one
proof
  let f be Function such that
A1: [:f,f:] is one-to-one;
  let x1,x2 be object such that
A2: x1 in dom f and
A3: x2 in dom f and
A4: f.x1 = f.x2;
A5: dom[:f,f:] = [:dom f,dom f:] by FUNCT_3:def 8;
  then
A6: [x1,x1] in dom[:f,f:] by A2,ZFMISC_1:87;
A7: [x2,x2] in dom[:f,f:] by A3,A5,ZFMISC_1:87;
  [:f,f:].(x1,x1) = [f.x2,f.x2] by A4,A5,A6,FUNCT_3:65
    .= [:f,f:].(x2,x2) by A5,A7,FUNCT_3:65;
  then [x1,x1] = [x2,x2] by A1,A6,A7;
  hence thesis by XTUPLE_0:1;
end;

theorem Th8:
  for f being Function st f is one-to-one holds ~f is one-to-one
proof
  let f be Function such that
A1: f is one-to-one;
  let x1,x2 be object;
  consider X,Y being set such that
A2: dom~f c= [:X,Y:] by FUNCT_4:44;
  assume
A3: x1 in dom~f;
  then consider x11,x12 being object such that x11 in X and x12 in Y and
A4: x1 = [x11,x12] by A2,ZFMISC_1:84;
  assume
A5: x2 in dom~f;
  then consider x21,x22 being object such that x21 in X and x22 in Y and
A6: x2 = [x21,x22] by A2,ZFMISC_1:84;
  assume
A7: (~f).x1 = (~f).x2;
A8: [x12,x11] in dom f by A3,A4,FUNCT_4:42;
A9: [x22,x21] in dom f by A5,A6,FUNCT_4:42;
  f.(x12,x11) = ~f.(x11,x12) by A3,A4,FUNCT_4:43
    .= (~f).(x21,x22) by A4,A6,A7
    .= f.(x22,x21) by A5,A6,FUNCT_4:43;
  then
A10: [x12,x11] = [x22,x21] by A1,A8,A9;
  then x12 = x22 by XTUPLE_0:1;
  hence thesis by A4,A6,A10,XTUPLE_0:1;
end;

theorem Th9:
  for f,g being Function st ~[:f,g:] is one-to-one holds [:g,f:] is one-to-one
proof
  let f,g be Function such that
A1: ~[:f,g:] is one-to-one;
  let x1,x2 be object;
A2: dom[:g,f:] = [:dom g, dom f:] by FUNCT_3:def 8;
A3: dom[:f,g:] = [:dom f, dom g:] by FUNCT_3:def 8;
  assume x1 in dom[:g,f:];
  then consider x11,x12 being object such that
A4: x11 in dom g and
A5: x12 in dom f and
A6: x1 = [x11,x12] by A2,ZFMISC_1:84;
  assume x2 in dom[:g,f:];
  then consider x21,x22 being object such that
A7: x21 in dom g and
A8: x22 in dom f and
A9: x2 = [x21,x22] by A2,ZFMISC_1:84;
  x1 in dom[:g,f:] by A2,A4,A5,A6,ZFMISC_1:87;
  then
A10: x1 in dom~[:f,g:] by A2,A3,FUNCT_4:46;
  x2 in dom[:g,f:] by A2,A7,A8,A9,ZFMISC_1:87;
  then
A11: x2 in dom~[:f,g:] by A2,A3,FUNCT_4:46;
  assume
A12: [:g,f:].x1 = [:g,f:].x2;
A13: [:g,f:].(x11,x12) = [g.x11,f.x12] by A4,A5,FUNCT_3:def 8;
A14: [:g,f:].(x21,x22) = [g.x21,f.x22] by A7,A8,FUNCT_3:def 8;
  then
A15: f.x22 = f.x12 by A6,A9,A12,A13,XTUPLE_0:1;
A16: g.x11 = g.x21 by A6,A9,A12,A13,A14,XTUPLE_0:1;
  (~[:f,g:]).[x11,x12] = (~[:f,g:]).(x11,x12)
    .= [:f,g:].(x12,x11) by A6,A10,FUNCT_4:43
    .= [f.x22,g.x21] by A4,A5,A15,A16,FUNCT_3:def 8
    .= [:f,g:].(x22,x21) by A7,A8,FUNCT_3:def 8
    .= (~[:f,g:]).(x21,x22) by A9,A11,FUNCT_4:43
    .= (~[:f,g:]).[x21,x22];
  hence thesis by A1,A6,A9,A10,A11;
end;

theorem Th10:
  for f,g being Function st f is one-to-one & g is one-to-one holds
  ~[:f,g:]" = ~([:g,f:]")
proof
  let f,g be Function such that
A1: f is one-to-one and
A2: g is one-to-one;
A3: [:g,f:]" = [:g",f":] by A1,A2,Th6;
  then
A4: dom([:g,f:]") = [:dom(g"), dom(f"):] by FUNCT_3:def 8;
A5: dom[:f,g:] = [:dom f, dom g:] by FUNCT_3:def 8;
A6: dom[:g,f:] = [:dom g, dom f:] by FUNCT_3:def 8;
A7: [:g,f:] is one-to-one by A1,A2;
A8: ~[:f,g:] is one-to-one by Th8,A1,A2;
A9: [:f,g:]" = [:f",g":] by A1,A2,Th6;
A10: dom~([:g,f:]") = [:dom(f"), dom(g"):] by A4,FUNCT_4:46
    .= dom [:f", g":] by FUNCT_3:def 8
    .= rng[:f,g:] by A1,A2,A9,FUNCT_1:32
    .= rng~[:f,g:] by A5,FUNCT_4:47;
  now
    let y,x be object;
    hereby
      assume that
A11:  y in rng~[:f,g:] and
A12:  x = (~([:g,f:]")).y;
      y in rng[:f,g:] by A5,A11,FUNCT_4:47;
      then y in [:rng f,rng g:] by FUNCT_3:67;
      then consider y1,y2 being object such that
A13:  y1 in rng f and
A14:  y2 in rng g and
A15:  y = [y1,y2] by ZFMISC_1:84;
      set x1 = f".y1, x2 = g".y2;
A16:  y2 in dom(g") by A2,A14,FUNCT_1:32;
A17:  y1 in dom(f") by A1,A13,FUNCT_1:32;
      then [y2,y1] in dom([:g,f:]") by A4,A16,ZFMISC_1:87;
      then
A18:  (~([:g,f:]")).(y1,y2) = [:g",f":].(y2,y1) by A3,FUNCT_4:def 2
        .= [x2,x1] by A16,A17,FUNCT_3:def 8;
A19:  y1 in dom(f") by A1,A13,FUNCT_1:32;
A20:  y2 in dom(g") by A2,A14,FUNCT_1:32;
A21:  x1 in rng(f") by A19,FUNCT_1:def 3;
A22:  x2 in rng(g") by A20,FUNCT_1:def 3;
A23:  x1 in dom f by A1,A21,FUNCT_1:33;
A24:  x2 in dom g by A2,A22,FUNCT_1:33;
      then
A25:  [x2,x1] in dom[:g,f:] by A6,A23,ZFMISC_1:87;
      then
A26:  [x2,x1] in dom~[:f,g:] by A5,A6,FUNCT_4:46;
      thus
      x in dom~[:f,g:] by A5,A6,A12,A15,A18,A25,FUNCT_4:46;
A27:  f.x1 = y1 by A1,A13,FUNCT_1:32;
A28:  g.x2 = y2 by A2,A14,FUNCT_1:32;
      thus (~[:f,g:]).x = ~[:f,g:].(x2,x1) by A12,A15,A18
        .= [:f,g:].(x1,x2) by A26,FUNCT_4:43
        .= y by A15,A23,A24,A27,A28,FUNCT_3:def 8;
    end;
    assume that
A29: x in dom~[:f,g:] and
A30: (~[:f,g:]).x = y;
    thus y in rng~[:f,g:] by A29,A30,FUNCT_1:def 3;
    x in dom[:g,f:] by A5,A6,A29,FUNCT_4:46;
    then consider x1,x2 being object such that
A31: x1 in dom g and
A32: x2 in dom f and
A33: x = [x1,x2] by A6,ZFMISC_1:84;
A34: (~[:f,g:]).(x1,x2) = [:f,g:].(x2,x1) by A29,A33,FUNCT_4:43
      .= [f.x2,g.x1] by A31,A32,FUNCT_3:def 8;
A35: g.x1 in rng g by A31,FUNCT_1:def 3;
    f.x2 in rng f by A32,FUNCT_1:def 3;
    then [g.x1,f.x2] in [:rng g, rng f:] by A35,ZFMISC_1:87;
    then [g.x1,f.x2] in rng[:g,f:] by FUNCT_3:67;
    then
A36: [g.x1,f.x2] in dom([:g,f:]") by A7,FUNCT_1:33;
    [x1,x2] in dom[:g,f:] by A6,A31,A32,ZFMISC_1:87;
    hence x = ([:g,f:]").([:g,f:].(x1,x2)) by A1,A2,A33,FUNCT_1:34
      .= ([:g,f:]").(g.x1,f.x2) by A31,A32,FUNCT_3:def 8
      .= (~([:g,f:]")).(f.x2,g.x1) by A36,FUNCT_4:def 2
      .= (~([:g,f:]")).y by A30,A33,A34;
  end;
  hence thesis by A8,A10,FUNCT_1:32;
end;

theorem Th11:
  for A,B be set, f being Function of A,B st f is onto
  holds id B c= [:f,f:].:id A
proof
  let A,B be set, f be Function of A,B;
  assume f is onto;
  then
A1: rng f = B;
  let xx be object;
  assume
A2: xx in id B;
  then consider x,x9 being object such that
A3: xx = [x,x9] by RELAT_1:def 1;
A4: x = x9 by A2,A3,RELAT_1:def 10;
A5: x in B by A2,A3,RELAT_1:def 10;
  then consider y being object such that
A6: y in A and
A7: f.y = x by A1,FUNCT_2:11;
A8: dom f = A by A5,FUNCT_2:def 1;
A9: [y,y] in id A by A6,RELAT_1:def 10;
  [:f,f:].(y,y) = xx by A3,A4,A6,A7,A8,FUNCT_3:def 8;
  hence thesis by A2,A9,FUNCT_2:35;
end;

theorem Th12:
  for F,G being Function-yielding Function, f be Function
  holds (G**F)*f = (G*f)**(F*f)
proof
  let F,G be Function-yielding Function, f be Function;
A1: dom((G**F)*f) = f"dom(G**F) by RELAT_1:147
    .= f"(dom G /\ dom F) by PBOOLE:def 19
    .= (f"dom F) /\ (f"dom G) by FUNCT_1:68
    .= (f"dom F) /\ dom(G*f) by RELAT_1:147
    .= dom(F*f) /\ dom(G*f) by RELAT_1:147;
  now
    let i be object;
    assume
A2: i in dom((G**F)*f);
    then
A3: i in dom f by FUNCT_1:11;
A4: f.i in dom(G**F) by A2,FUNCT_1:11;
    thus ((G**F)*f).i = (G**F).(f.i) by A2,FUNCT_1:12
      .= (G.(f.i))*(F.(f.i)) by A4,PBOOLE:def 19
      .= ((G*f).i)*(F.(f.i)) by A3,FUNCT_1:13
      .= ((G*f).i)*((F*f).i) by A3,FUNCT_1:13;
  end;
  hence thesis by A1,PBOOLE:def 19;
end;

theorem Th13:
  for A,B,C being set, f being Function of [:A,B:],C st ~f is onto
  holds f is onto
proof
  let A,B,C be set, f be Function of [:A,B:],C;
A1: rng~f c= rng f by FUNCT_4:41;
  assume ~f is onto;
  then rng~f = C;
  hence rng f = C by A1;
end;

theorem Th14:
  for A be set, B being non empty set, f being Function of A,B
  holds [:f,f:].:id A c= id B
proof
  let A be set, B be non empty set, f be Function of A,B;
  let x be object;
  assume x in [:f,f:].:id A;
  then consider yy being object such that
A1: yy in [:A,A:] and
A2: yy in id A and
A3: [:f,f:].yy = x by FUNCT_2:64;
  consider y,y9 being object such that
A4: y in A and y9 in A and
A5: yy = [y,y9] by A1,ZFMISC_1:84;
A6: y = y9 by A2,A5,RELAT_1:def 10;
  reconsider y as Element of A by A4;
A7: f.y in B by A4,FUNCT_2:5;
A8: y in dom f by A4,FUNCT_2:def 1;
  x = [:f,f:].(y,y9) by A3,A5
    .= [f.y,f.y] by A6,A8,FUNCT_3:def 8;
  hence thesis by A7,RELAT_1:def 10;
end;

begin :: Functions bewteen Cartesian products

definition
  let A,B be set;
  mode bifunction of A,B is Function of [:A,A:],[:B,B:];
end;

definition
  let A,B be set, f be bifunction of A,B;

  attr f is Covariant means
  :Def1:
  ex g being Function of A,B st f = [:g,g:];
  attr f is Contravariant means
  :Def2:
  ex g being Function of A,B st f = ~[:g,g:];
end;

theorem Th15:
  for A be set, B be non empty set,
  b being Element of B, f being bifunction of A,B st f = [:A,A:] --> [b,b]
  holds f is Covariant Contravariant
proof
  let A be set, B be non empty set,
  b be Element of B, f be bifunction of A,B such that
A1: f = [:A,A:] --> [b,b];
  reconsider g = A --> b as Function of A,B;
  thus f is Covariant
  proof
    take g;
    thus thesis by A1,ALTCAT_2:1;
  end;
  take g;
  [:A,A:] --> [b,b] = ~([:A,A:] --> [b,b]) by Th5;
  hence thesis by A1,ALTCAT_2:1;
end;

registration
  let A,B be set;
  cluster Covariant Contravariant for bifunction of A,B;
  existence
  proof
    per cases;
    suppose
A1:   B = {};
      then [:B,B:] = {} by ZFMISC_1:90;
      then reconsider f = {} as bifunction of A,B by Th1;
      take f;
      reconsider g = {} as Function of A,B by A1,Th1;
      reconsider h = g as empty Function;
      thus f is Covariant
      proof
        take g;
        thus f = [:h,h:] .= [:g,g:];
      end;
      take g;
      thus f = ~[:h,h:] .= ~[:g,g:];
    end;
    suppose
A2:   B <> {};
      set b = the Element of B;
      set f = [:A,A:] --> [b,b];
      [b,b] in [:B,B:] by A2,ZFMISC_1:87;
      then reconsider f as bifunction of A,B by FUNCOP_1:45;
      take f;
      thus thesis by A2,Th15;
    end;
  end;
end;

theorem
  for A,B being non empty set
  for f being Covariant Contravariant bifunction of A,B
  ex b being Element of B st f = [:A,A:] --> [b,b]
proof
  let A,B be non empty set;
  let f be Covariant Contravariant bifunction of A,B;
  consider g1 being Function of A,B such that
A1: f = [:g1,g1:] by Def1;
  consider g2 being Function of A,B such that
A2: f = ~[:g2,g2:] by Def2;
  set a = the Element of A;
  take b = g1.a;
A3: dom f = [:A,A:] by FUNCT_2:def 1;
  now
    let z be object;
    assume z in dom f;
    then consider a1,a2 being Element of A such that
A4: z = [a1,a2] by DOMAIN_1:1;
A5: dom g2 = A by FUNCT_2:def 1;
A6: dom g1 = A by FUNCT_2:def 1;
A7: dom[:g2,g2:] = [:dom g2, dom g2:] by FUNCT_3:def 8;
    then
A8: [a1,a] in dom[:g2,g2:] by A5,ZFMISC_1:87;
A9: dom g2 = A by FUNCT_2:def 1;
    [b,g1.a1] = f.(a,a1) by A1,A6,FUNCT_3:def 8
      .= [:g2,g2:].(a1,a) by A2,A8,FUNCT_4:def 2
      .= [g2.a1,g2.a] by A9,FUNCT_3:def 8;
    then
A10: g2.a1 = b by XTUPLE_0:1;
A11: [a2,a] in dom[:g2,g2:] by A5,A7,ZFMISC_1:87;
    [b,g1.a2] = f.(a,a2) by A1,A6,FUNCT_3:def 8
      .= [:g2,g2:].(a2,a) by A2,A11,FUNCT_4:def 2
      .= [g2.a2,g2.a] by A9,FUNCT_3:def 8;
    then
A12: g2.a2 = b by XTUPLE_0:1;
A13: [a2,a1] in dom[:g2,g2:] by A5,A7,ZFMISC_1:87;
    thus f.z = [:g1,g1:].(a1,a2) by A1,A4
      .= [:g2,g2:].(a2,a1) by A1,A2,A13,FUNCT_4:def 2
      .= [b,b] by A9,A10,A12,FUNCT_3:def 8;
  end;
  hence thesis by A3,FUNCOP_1:11;
end;

begin :: Unary transformatiom

definition
  let I1,I2 be set, f be Function of I1,I2;
  let A be ManySortedSet of I1, B be ManySortedSet of I2;
  mode MSUnTrans of f,A,B -> ManySortedSet of I1 means
    :Def3:
    ex I29 being non empty set, B9 being ManySortedSet of I29,
    f9 being Function of I1,I29 st f = f9 & B = B9 &
    it is ManySortedFunction of A,B9*f9 if I2 <> {} otherwise it = EmptyMS I1;
  existence
  proof
    hereby
      assume I2 <> {};
      then reconsider I29 = I2 as non empty set;
      reconsider f9 = f as Function of I1,I29;
      reconsider B9 = B as ManySortedSet of I29;
      set IT = the ManySortedFunction of A,B9*f9;
      reconsider IT9 = IT as ManySortedSet of I1;
      take IT9,I29;
      reconsider f9 = f as Function of I1,I29;
      reconsider B9 = B as ManySortedSet of I29;
      take B9,f9;
      thus f = f9 & B = B9;
      thus IT9 is ManySortedFunction of A,B9*f9;
    end;
    thus thesis;
  end;
  consistency;
end;

definition
  let I1 be set, I2 be non empty set, f be Function of I1,I2;
  let A be ManySortedSet of I1, B be ManySortedSet of I2;
  redefine mode MSUnTrans of f,A,B means
    :Def4:
    it is ManySortedFunction of A,B*f;
  compatibility
  proof
    let M be ManySortedSet of I1;
    hereby
      assume M is MSUnTrans of f,A,B;
      then ex I29 being non empty set, B9 being ManySortedSet of I29,
      f9 being Function of I1,I29 st f = f9 & B = B9 &
      M is ManySortedFunction of A,B9*f9 by Def3;
      hence M is ManySortedFunction of A,B*f;
    end;
    thus thesis by Def3;
  end;
end;

registration
  let I1,I2 be set;
  let f be Function of I1,I2;
  let A be ManySortedSet of I1, B be ManySortedSet of I2;
  cluster -> Function-yielding for MSUnTrans of f,A,B;
  coherence
  proof
    let M be MSUnTrans of f,A,B;
    per cases;
    suppose I2 <> {};
      then ex I29 being non empty set, B9 being ManySortedSet of I29,
      f9 being Function of I1,I29 st f = f9 & B = B9 &
      M is ManySortedFunction of A,B9*f9 by Def3;
      hence thesis;
    end;
    suppose I2 = {};
      then M = EmptyMS I1 by Def3;
      hence thesis;
    end;
  end;
end;

theorem Th17:
  for I1 being set, I2,I3 being non empty set,
  f being Function of I1,I2, g being Function of I2,I3,
  B being ManySortedSet of I2, C being ManySortedSet of I3,
  G being MSUnTrans of g,B,C holds G*f is MSUnTrans of g*f,B*f,C
proof
  let I1 be set, I2,I3 be non empty set,
  f be Function of I1,I2, g be Function of I2,I3,
  B be ManySortedSet of I2, C be ManySortedSet of I3, G be MSUnTrans of g,B,C;
A1: C*(g*f) = C*g*f by RELAT_1:36;
  G is ManySortedFunction of B,C*g by Def4;
  hence G*f is ManySortedFunction of B*f,C*(g*f) by A1,ALTCAT_2:5;
end;

definition
  let I1 be set, I2 be non empty set, f be Function of I1,I2,
  A be ManySortedSet of [:I1,I1:], B be ManySortedSet of [:I2,I2:],
  F be MSUnTrans of [:f,f:],A,B;
  redefine func ~F -> MSUnTrans of [:f,f:],~A,~B;
  coherence
  proof
    reconsider G = F as ManySortedFunction of A,B*[:f,f:] by Def4;
    ~G is ManySortedFunction of ~A,~B*[:f,f:] by ALTCAT_2:3;
    hence ~F is MSUnTrans of [:f,f:],~A,~B by Def4;
  end;
end;

theorem Th18:
  for I1,I2 being non empty set,
  A being ManySortedSet of I1, B being ManySortedSet of I2,
  o being Element of I2 st B.o <> {}
  for m being Element of B.o, f being Function of I1,I2 st f = I1 --> o holds
  the set of all  [o9,A.o9 --> m] where o9 is Element of I1
  is MSUnTrans of f,A,B
proof
  let I1,I2 be non empty set,
  A be ManySortedSet of I1, B be ManySortedSet of I2,
  o be Element of I2 such that
A1: B.o <> {};
  let m be Element of B.o, f be Function of I1,I2 such that
A2: f = I1 --> o;
  defpred P[set] means not contradiction;
  deffunc F(set) = A.$1 --> m;
  reconsider Xm = { [o9,F(o9)] where o9 is Element of I1:
  P[o9] } as Function from ALTCAT_2:sch 1;
A3: Xm = { [o9,F(o9)] where o9 is Element of I1: P[o9] };
  dom Xm = { o9 where o9 is Element of I1: P[o9] } from ALTCAT_2:sch 2(
  A3)
    .= I1 by DOMAIN_1:18;
  then reconsider Xm as ManySortedSet of I1 by PARTFUN1:def 2,RELAT_1:def 18;
  deffunc F(set) = A.$1 --> m;
A4: Xm = { [o9,F(o9)] where o9 is Element of I1: P[o9] };
  now
    let i be object;
    assume
A5: i in I1;
    then reconsider o9 = i as Element of I1;
A6: P[o9];
A7: i in dom f by A2,A5;
    f.i = o by A2,A5,FUNCOP_1:7;
    then m in B.(f.i) by A1;
    then
A8: m in (B*f).i by A7,FUNCT_1:13;
    Xm.o9 = F(o9) from ALTCAT_2:sch 3(A4,A6);
    hence Xm.i is Function of A.i, (B*f).i by A8,FUNCOP_1:45;
  end;
  then Xm is ManySortedFunction of A,B*f by PBOOLE:def 15;
  hence thesis by Def4;
end;

theorem Th19:
  for I1 being set, I2,I3 being non empty set,
  f being Function of I1,I2, g being Function of I2,I3,
  A being ManySortedSet of I1, B being ManySortedSet of I2,
  C being ManySortedSet of I3, F being MSUnTrans of f,A,B,
  G being MSUnTrans of g*f,B*f,C
  st for ii being set st ii in I1 & (B*f).ii = {}
  holds A.ii = {} or (C*(g*f)).ii = {}
  holds G**(F qua Function-yielding Function) is MSUnTrans of g*f,A,C
proof
  let I1 be set, I2,I3 be non empty set,
  f be Function of I1,I2, g be Function of I2,I3,
  A be ManySortedSet of I1, B be ManySortedSet of I2,
  C be ManySortedSet of I3, F be MSUnTrans of f,A,B,
  G be MSUnTrans of g*f,B*f,C such that
A1: for ii being set st ii in I1 & (B*f).ii = {}
  holds A.ii = {} or (C*(g*f)).ii = {};
  reconsider G as ManySortedFunction of B*f,C*(g*f) by Def4;
  reconsider F as ManySortedFunction of A,B*f by Def4;
A2: dom G = I1 by PARTFUN1:def 2;
A3: dom F = I1 by PARTFUN1:def 2;
A4: dom(G**F) = dom G /\ dom F by PBOOLE:def 19
    .= I1 by A2,A3;
  reconsider GF = G**F as ManySortedSet of I1;
  GF is ManySortedFunction of A,C*(g*f)
  proof
    let ii be object;
    assume
A5: ii in I1;
    then reconsider Fi = F.ii as Function of A.ii, (B*f).ii by PBOOLE:def 15;
    reconsider Gi = G.ii as Function of (B*f).ii, (C*(g*f)).ii
    by A5,PBOOLE:def 15;
    (B*f).ii = {} implies A.ii = {} or (C*(g*f)).ii = {} by A1,A5;
    then Gi*Fi is Function of A.ii, (C*(g*f)).ii by FUNCT_2:13;
    hence thesis by A4,A5,PBOOLE:def 19;
  end;
  hence thesis by Def4;
end;

begin :: Functors

definition
  let C1,C2 be 1-sorted;
  struct BimapStr over C1,C2
  (#ObjectMap -> bifunction of the carrier of C1, the carrier of C2 #);
end;

definition
  let C1,C2 be non empty AltGraph;
  let F be BimapStr over C1,C2;
  let o be Object of C1;
  func F.o -> Object of C2 equals
  ((the ObjectMap of F).(o,o))`1;
  coherence by MCART_1:10;
end;

definition
  let A,B be 1-sorted, F be BimapStr over A,B;
  attr F is one-to-one means

  the ObjectMap of F is one-to-one;
  attr F is onto means

  the ObjectMap of F is onto;
  attr F is reflexive means

  (the ObjectMap of F).:id the carrier of A c= id the carrier of B;
  attr F is coreflexive means

  id the carrier of B c= (the ObjectMap of F).:id the carrier of A;
end;

definition
  let A,B be non empty AltGraph, F be BimapStr over A,B;
  redefine attr F is reflexive means
  :Def10:
  for o being Object of A holds (the ObjectMap of F).(o,o) = [F.o,F.o];
  compatibility
  proof
    hereby
      assume F is reflexive;
      then
      A1:   (
the ObjectMap of F).:id the carrier of A c= id the carrier of B;
      let o be Object of A;
      [o,o] in id the carrier of A by RELAT_1:def 10;
      then
A2:   (the ObjectMap of F).(o,o) in
      (the ObjectMap of F).:id the carrier of A by FUNCT_2:35;
      consider p,p9 being object such that
A3:   (the ObjectMap of F).(o,o) = [p,p9] by RELAT_1:def 1;
      thus (the ObjectMap of F).(o,o) = [F.o,F.o] by A1,A2,A3,RELAT_1:def 10;
    end;
    assume
A4: for o being Object of A holds (the ObjectMap of F).(o,o) = [F.o,F.o];
    let x be object;
    assume x in (the ObjectMap of F).:id the carrier of A;
    then consider y being object such that
A5: y in [:the carrier of A,the carrier of A:] and
A6: y in id the carrier of A and
A7: x = (the ObjectMap of F).y by FUNCT_2:64;
    consider o,o9 being Element of A such that
A8: y = [o,o9] by A5,DOMAIN_1:1;
    reconsider o as Object of A;
    o = o9 by A6,A8,RELAT_1:def 10;
    then x = [F.o,F.o] by A4,A7,A8;
    hence thesis by RELAT_1:def 10;
  end;
end;

theorem Th20:
  for A,B being reflexive non empty AltGraph,
  F being BimapStr over A,B st F is coreflexive for o being Object of B
  ex o9 being Object of A st F.o9 = o
proof
  let A,B be reflexive non empty AltGraph, F be BimapStr over A,B;
  assume F is coreflexive;
  then
A1: id the carrier of B c= (the ObjectMap of F).:id the carrier of A;
  let o be Object of B;
  reconsider oo = [o,o] as
  Element of [:the carrier of B,the carrier of B:] by ZFMISC_1:87;
  [o,o] in id the carrier of B by RELAT_1:def 10;
  then consider pp being Element of [:the carrier of A,the carrier of A:]
  such that
A2: pp in id the carrier of A and
A3: (the ObjectMap of F).pp = oo by A1,FUNCT_2:65;
  consider p,p9 being object such that
A4: pp = [p,p9] by RELAT_1:def 1;
A5: p = p9 by A2,A4,RELAT_1:def 10;
  reconsider p as Object of A by A2,A4,RELAT_1:def 10;
  take p;
  thus thesis by A3,A4,A5;
end;

definition
  let C1, C2 be non empty AltGraph;
  let F be BimapStr over C1,C2;
  attr F is feasible means
  :Def11:
  for o1,o2 being Object of C1 st <^o1,o2^> <> {} holds
  (the Arrows of C2).((the ObjectMap of F).(o1,o2)) <> {};
end;

definition
  let C1,C2 be AltGraph;
  struct(BimapStr over C1,C2) FunctorStr over C1,C2
  (#ObjectMap -> bifunction of the carrier of C1,the carrier of C2,
    MorphMap ->
    MSUnTrans of the ObjectMap, the Arrows of C1, the Arrows of C2 #);
end;

definition
  let C1,C2 be 1-sorted;
  let IT be BimapStr over C1,C2;
  attr IT is Covariant means
  :Def12:
  the ObjectMap of IT is Covariant;
  attr IT is Contravariant means
  :Def13:
  the ObjectMap of IT is Contravariant;
end;

registration
  let C1,C2 be AltGraph;
  cluster Covariant for FunctorStr over C1,C2;
  existence
  proof
    set f = the Covariant bifunction of the carrier of C1, the carrier of C2;
    set M = the MSUnTrans of f, the Arrows of C1, the Arrows of C2;
    take F = FunctorStr(#f,M#);
    thus the ObjectMap of F is Covariant;
  end;
  cluster Contravariant for FunctorStr over C1,C2;
  existence
  proof

set f = the Contravariant bifunction of the carrier of C1, the carrier of C2;
    set M = the MSUnTrans of f, the Arrows of C1, the Arrows of C2;
    take F = FunctorStr(#f,M#);
    thus the ObjectMap of F is Contravariant;
  end;
end;

definition
  let C1,C2 be AltGraph;
  let F be FunctorStr over C1,C2;
  let o1,o2 be Object of C1;
  func Morph-Map(F,o1,o2) -> set equals
  (the MorphMap of F).(o1,o2);
  correctness;
end;

registration
  let C1,C2 be AltGraph;
  let F be FunctorStr over C1,C2;
  let o1,o2 be Object of C1;
  cluster Morph-Map(F,o1,o2) -> Relation-like Function-like;
  coherence;
end;

definition
  let C1,C2 be non empty AltGraph;
  let F be Covariant FunctorStr over C1,C2;
  let o1,o2 be Object of C1;
  redefine func Morph-Map(F,o1,o2) -> Function of <^o1,o2^>, <^F.o1,F.o2^>;
  coherence
  proof
    consider I29 being non empty set, B9 being ManySortedSet of I29,
    f9 being Function of [:the carrier of C1,the carrier of C1:],I29 such that
A1: the ObjectMap of F = f9 and
A2: the Arrows of C2 = B9 and
A3: the MorphMap of F is ManySortedFunction of the Arrows of C1,B9*f9 by Def3;
A4: (the Arrows of C1).[o1,o2] = (the Arrows of C1).(o1,o2)
      .= <^o1,o2^> by ALTCAT_1:def 1;
A5: [o1,o2] in [:the carrier of C1, the carrier of C1:] by ZFMISC_1:87;
    the ObjectMap of F is Covariant by Def12;
    then consider g being Function of the carrier of C1, the carrier of C2
    such that
A6: the ObjectMap of F = [:g,g:];
A7: F.o1 = [g.o1,g.o1]`1 by A6,FUNCT_3:75
      .= g.o1;
A8: F.o2 = [g.o2,g.o2]`1 by A6,FUNCT_3:75
      .= g.o2;
    dom f9 = [:the carrier of C1, the carrier of C1:] by FUNCT_2:def 1;
    then (B9*f9).[o1,o2] = B9.(f9.(o1,o2)) by A5,FUNCT_1:13
      .= (the Arrows of C2).(F.o1,F.o2) by A1,A2,A6,A7,A8,FUNCT_3:75
      .= <^F.o1,F.o2^> by ALTCAT_1:def 1;
    hence thesis by A3,A4,A5,PBOOLE:def 15;
  end;
end;

definition
  let C1,C2 be non empty AltGraph;
  let F be Covariant FunctorStr over C1,C2;
  let o1,o2 be Object of C1 such that
A1: <^o1,o2^> <> {} and
A2: <^F.o1,F.o2^> <> {};
  let m be Morphism of o1,o2;
  func F.m -> Morphism of F.o1, F.o2 equals
  :Def15:
  Morph-Map(F,o1,o2).m;
  coherence
  proof
    reconsider A = <^o1,o2^>, B = <^F.o1,F.o2^> as non empty set by A1,A2;
    reconsider M = Morph-Map(F,o1,o2) as Function of A,B;
    reconsider m as Element of A;
    M.m is Element of B;
    hence thesis;
  end;
end;

definition
  let C1,C2 be non empty AltGraph;
  let F be Contravariant FunctorStr over C1,C2;
  let o1,o2 be Object of C1;
  redefine func Morph-Map(F,o1,o2) -> Function of <^o1,o2^>, <^F.o2,F.o1^>;
  coherence
  proof
    consider I29 being non empty set, B9 being ManySortedSet of I29,
    f9 being Function of [:the carrier of C1,the carrier of C1:],I29 such that
A1: the ObjectMap of F = f9 and
A2: the Arrows of C2 = B9 and
A3: the MorphMap of F is ManySortedFunction of the Arrows of C1,B9*f9 by Def3;
A4: (the Arrows of C1).[o1,o2] = (the Arrows of C1).(o1,o2)
      .= <^o1,o2^> by ALTCAT_1:def 1;
A5: [o1,o2] in [:the carrier of C1, the carrier of C1:] by ZFMISC_1:87;
    the ObjectMap of F is Contravariant by Def13;
    then consider g being Function of the carrier of C1, the carrier of C2
    such that
A6: the ObjectMap of F = ~[:g,g:];
A7: dom f9 = [:the carrier of C1, the carrier of C1:] by FUNCT_2:def 1;
    then [o1,o1] in dom~[:g,g:] by A1,A6,ZFMISC_1:87;
    then [o1,o1] in dom[:g,g:] by FUNCT_4:42;
    then
A8: F.o1 = ([:g,g:].(o1,o1))`1 by A6,FUNCT_4:def 2
      .= [g.o1,g.o1]`1 by FUNCT_3:75
      .= g.o1;
    [o2,o2] in dom~[:g,g:] by A1,A6,A7,ZFMISC_1:87;
    then [o2,o2] in dom[:g,g:] by FUNCT_4:42;
    then
A9: F.o2 = ([:g,g:].(o2,o2))`1 by A6,FUNCT_4:def 2
      .= [g.o2,g.o2]`1 by FUNCT_3:75
      .= g.o2;
    [o1,o2] in dom~[:g,g:] by A1,A6,A7,ZFMISC_1:87;
    then
A10: [o2,o1] in dom[:g,g:] by FUNCT_4:42;
    (B9*f9).[o1,o2] = B9.(f9.(o1,o2)) by A5,A7,FUNCT_1:13
      .= B9.([:g,g:].(o2,o1)) by A1,A6,A10,FUNCT_4:def 2
      .= (the Arrows of C2).(F.o2,F.o1) by A2,A8,A9,FUNCT_3:75
      .= <^F.o2,F.o1^> by ALTCAT_1:def 1;
    hence thesis by A3,A4,A5,PBOOLE:def 15;
  end;
end;

definition
  let C1,C2 be non empty AltGraph;
  let F be Contravariant FunctorStr over C1,C2;
  let o1,o2 be Object of C1 such that
A1: <^o1,o2^> <> {} and
A2: <^F.o2,F.o1^> <> {};
  let m be Morphism of o1,o2;
  func F.m -> Morphism of F.o2, F.o1 equals
  :Def16:
  Morph-Map(F,o1,o2).m;
  coherence
  proof
    reconsider A = <^o1,o2^>, B = <^F.o2,F.o1^> as non empty set by A1,A2;
    reconsider M = Morph-Map(F,o1,o2) as Function of A,B;
    reconsider m as Element of A;
    M.m is Element of B;
    hence thesis;
  end;
end;

definition
  let C1,C2 be non empty AltGraph;
  let o be Object of C2 such that
A1: <^o,o^> <> {};
  let m be Morphism of o,o;
  func C1 --> m -> strict FunctorStr over C1,C2 means
  :Def17:
  the ObjectMap of it = [:the carrier of C1,the carrier of C1:] --> [o,o] &
  the MorphMap of it =
  the set of all
 [[o1,o2],<^o1,o2^> --> m] where o1 is Object of C1, o2 is Object of C1;
  existence
  proof
    set I1 = [:the carrier of C1,the carrier of C1:],
    I2 = [:the carrier of C2,the carrier of C2:],
    A = the Arrows of C1, B = the Arrows of C2;
    reconsider oo = [o,o] as Element of I2 by ZFMISC_1:87;
    B.oo = B.(o,o) .= <^o,o^> by ALTCAT_1:def 1;
    then reconsider m as Element of B.oo;
    reconsider f = I1 --> oo as Function of I1, I2;
    reconsider f as bifunction of the carrier of C1,the carrier of C2;
    set M = the set of all  [[o1,o2],<^o1,o2^> --> m]
    where o1 is Object of C1, o2 is Object of C1;
A2: M = the set of all  [o9,A.o9 --> m] where o9 is Element of I1
    proof
      thus M c=
      the set of all  [o9,A.o9 --> m] where o9 is Element of I1
      proof
        let x be object;
        assume x in M;
        then consider o3,o4 being Object of C1 such that
A3:     x = [[o3,o4],<^o3,o4^> --> m];
        reconsider oo = [o3,o4] as Element of I1 by ZFMISC_1:87;
        x = [oo,A.(o3,o4) --> m] by A3,ALTCAT_1:def 1
          .= [oo,A.oo --> m];
        hence thesis;
      end;
      let x be object;
      assume x in the set of all  [o9,A.o9 --> m] where o9 is Element of I1;
      then consider o9 being Element of I1 such that
A4:   x = [o9,A.o9 --> m];
      reconsider o1 = o9`1, o2 = o9`2 as Element of C1 by MCART_1:10;
      reconsider o1, o2 as Object of C1;
      o9 = [o1,o2] by MCART_1:21;
      then x = [[o1,o2],A.(o1,o2) --> m] by A4
        .= [[o1,o2],<^o1,o2^> --> m] by ALTCAT_1:def 1;
      hence thesis;
    end;
    B.(o,o) <> {} by A1,ALTCAT_1:def 1;
    then reconsider M as MSUnTrans of f, A, B by A2,Th18;
    take FunctorStr(#f,M#);
    thus thesis;
  end;
  uniqueness;
end;

theorem Th21:
  for C1,C2 being non empty AltGraph, o2 being Object of C2 st <^o2,o2^> <> {}
  for m be Morphism of o2,o2, o1 being Object of C1 holds (C1 --> m).o1 = o2
proof
  let C1,C2 be non empty AltGraph, o2 be Object of C2 such that
A1: <^o2,o2^> <> {};
  let m be Morphism of o2,o2, o1 be Object of C1;
A2: [o1,o1] in [:the carrier of C1,the carrier of C1:] by ZFMISC_1:87;
  thus (C1 --> m).o1 =
  (([:the carrier of C1,the carrier of C1:] --> [o2,o2]).(o1,o1))`1
  by A1,Def17
    .= [o2,o2]`1 by A2,FUNCOP_1:7
    .= o2;
end;

registration
  let C1 be non empty AltGraph, C2 be non empty reflexive AltGraph;
  let o be Object of C2, m be Morphism of o,o;
  cluster C1 --> m -> Covariant Contravariant feasible;
  coherence
  proof
    <^o,o^> <> {} by ALTCAT_2:def 7;
    then
A1: the ObjectMap of C1 --> m
    = [:the carrier of C1,the carrier of C1:] --> [o,o] by Def17;
    hence the ObjectMap of C1 --> m is Covariant Contravariant by Th15;
    let o1,o2 be Object of C1 such that <^o1,o2^> <> {};
    [o1,o2] in [:the carrier of C1,the carrier of C1:] by ZFMISC_1:87;
    then (the Arrows of C2).((the ObjectMap of C1 --> m).(o1,o2))
    = (the Arrows of C2).(o,o) by A1,FUNCOP_1:7;
    hence thesis by ALTCAT_2:def 6;
  end;
end;

registration
  let C1 be non empty AltGraph, C2 be non empty reflexive AltGraph;
  cluster feasible Covariant Contravariant for FunctorStr over C1,C2;
  existence
  proof set o = the Object of C2;
    set m = the Morphism of o,o;
    take C1 --> m;
    thus thesis;
  end;
end;

theorem Th22:
  for C1, C2 being non empty AltGraph,
  F being Covariant FunctorStr over C1,C2, o1,o2 being Object of C1
  holds (the ObjectMap of F).(o1,o2) = [F.o1,F.o2]
proof
  let C1, C2 be non empty AltGraph, F be Covariant FunctorStr over C1,C2,
  o1,o2 be Object of C1;
  the ObjectMap of F is Covariant by Def12;
  then consider f being Function of the carrier of C1, the carrier of C2 such
  that
A1: the ObjectMap of F = [:f,f:];
A2: F.o1 = ([f.o1,f.o1])`1 by A1,FUNCT_3:75
    .= f.o1;
  F.o2 = ([f.o2,f.o2])`1 by A1,FUNCT_3:75
    .= f.o2;
  hence thesis by A1,A2,FUNCT_3:75;
end;

definition
  let C1, C2 be non empty AltGraph;
  let F be Covariant FunctorStr over C1,C2;
  redefine attr F is feasible means
  :Def18:
  for o1,o2 being Object of C1 st <^o1,o2^> <> {} holds <^F.o1,F.o2^> <> {};
  compatibility
  proof
    hereby
      assume
A1:   F is feasible;
      let o1,o2 be Object of C1;
      assume
A2:   <^o1,o2^> <> {};
      <^F.o1,F.o2^> = (the Arrows of C2).(F.o1,F.o2) by ALTCAT_1:def 1
        .= (the Arrows of C2).((the ObjectMap of F).(o1,o2)) by Th22;
      hence <^F.o1,F.o2^> <> {} by A1,A2;
    end;
    assume
    A3: for
 o1,o2 being Object of C1 st <^o1,o2^> <> {} holds <^F.o1,F.o2^> <> {};
    let o1,o2 be Object of C1;
    assume
A4: <^o1,o2^> <> {};
    <^F.o1,F.o2^> = (the Arrows of C2).(F.o1,F.o2) by ALTCAT_1:def 1
      .= (the Arrows of C2).((the ObjectMap of F).(o1,o2)) by Th22;
    hence thesis by A3,A4;
  end;
end;

theorem Th23:
  for C1, C2 being non empty AltGraph,
  F being Contravariant FunctorStr over C1,C2, o1,o2 being Object of C1
  holds (the ObjectMap of F).(o1,o2) = [F.o2,F.o1]
proof
  let C1, C2 be non empty AltGraph, F be Contravariant FunctorStr over C1,C2,
  o1,o2 be Object of C1;
  the ObjectMap of F is Contravariant by Def13;
  then consider f being Function of the carrier of C1, the carrier of C2 such
  that
A1: the ObjectMap of F = ~[:f,f:];
A2: dom[:f,f:] = [:the carrier of C1, the carrier of C1:] by FUNCT_2:def 1;
  then [o1,o1] in dom[:f,f:] by ZFMISC_1:87;
  then
A3: F.o1 = ([:f,f:].(o1,o1))`1 by A1,FUNCT_4:def 2
    .= ([f.o1,f.o1])`1 by FUNCT_3:75
    .= f.o1;
  [o2,o2] in dom[:f,f:] by A2,ZFMISC_1:87;
  then
A4: F.o2 = ([:f,f:].(o2,o2))`1 by A1,FUNCT_4:def 2
    .= ([f.o2,f.o2])`1 by FUNCT_3:75
    .= f.o2;
  [o2,o1] in dom[:f,f:] by A2,ZFMISC_1:87;
  hence (the ObjectMap of F).(o1,o2) = [:f,f:].(o2,o1) by A1,FUNCT_4:def 2
    .= [F.o2,F.o1] by A3,A4,FUNCT_3:75;
end;

definition
  let C1, C2 be non empty AltGraph;
  let F be Contravariant FunctorStr over C1,C2;
  redefine attr F is feasible means
  :Def19:
  for o1,o2 being Object of C1 st <^o1,o2^> <> {} holds <^F.o2,F.o1^> <> {};
  compatibility
  proof
    hereby
      assume
A1:   F is feasible;
      let o1,o2 be Object of C1;
      assume
A2:   <^o1,o2^> <> {};
      <^F.o2,F.o1^> = (the Arrows of C2).(F.o2,F.o1) by ALTCAT_1:def 1
        .= (the Arrows of C2).((the ObjectMap of F).(o1,o2)) by Th23;
      hence <^F.o2,F.o1^> <> {} by A1,A2;
    end;
    assume
    A3: for
 o1,o2 being Object of C1 st <^o1,o2^> <> {} holds <^F.o2,F.o1^> <> {};
    let o1,o2 be Object of C1;
    assume
A4: <^o1,o2^> <> {};
    <^F.o2,F.o1^> = (the Arrows of C2).(F.o2,F.o1) by ALTCAT_1:def 1
      .= (the Arrows of C2).((the ObjectMap of F).(o1,o2)) by Th23;
    hence thesis by A3,A4;
  end;
end;

registration
  let C1,C2 be AltGraph;
  let F be FunctorStr over C1,C2;
  cluster the MorphMap of F -> Function-yielding;
  coherence;
end;

registration
  cluster non empty reflexive for AltCatStr;
  existence
  proof set C = the category;
    take C;
    thus thesis;
  end;
end;

:: Wlasnosci funktorow, Semadeni-Wiweger str. 32

definition
  let C1,C2 be with_units non empty AltCatStr;
  let F be FunctorStr over C1,C2;
  attr F is id-preserving means
  :Def20:
  for o being Object of C1 holds Morph-Map(F,o,o).idm o = idm F.o;
end;

theorem Th24:
  for C1,C2 being non empty AltGraph, o2 being Object of C2 st <^o2,o2^> <> {}
  for m be Morphism of o2,o2, o,o9 being Object of C1, f being Morphism of o,o9
  st <^o,o9^> <> {} holds Morph-Map(C1 --> m,o,o9).f = m
proof
  let C1,C2 be non empty AltGraph, o2 be Object of C2 such that
A1: <^o2,o2^> <> {};
  let m be Morphism of o2,o2, o,o9 be Object of C1, f be Morphism of o,o9
  such that
A2: <^o,o9^> <> {};
  set X =
  the set of all
 [[o1,o19],<^o1,o19^> --> m] where o1 is Object of C1, o19 is Object of C1;
 set Y = the set of all  [[o1,o19],(the Arrows of C1).(o1,o19) --> m]
  where o1 is Element of C1, o19 is Element of C1;
A3: X c= Y
  proof
    let e be object;
    assume e in X;
    then consider o1,o19 being Object of C1 such that
A4: e = [[o1,o19],<^o1,o19^> --> m];
    e = [[o1,o19],(the Arrows of C1).(o1,o19) --> m] by A4,ALTCAT_1:def 1;
    hence thesis;
  end;
A5: Y c= X
  proof
    let e be object;
    assume e in Y;
    then consider o1,o19 being Element of C1 such that
A6: e = [[o1,o19],(the Arrows of C1).(o1,o19) --> m];
    reconsider o1,o19 as Object of C1;
    e = [[o1,o19],<^o1,o19^> --> m] by A6,ALTCAT_1:def 1;
    hence thesis;
  end;
  defpred P[set,set] means not contradiction;
  deffunc F(Element of C1,Element of C1) = (the Arrows of C1).($1,$2) --> m;
  the MorphMap of C1 --> m = X by A1,Def17;
  then
A7: the MorphMap of C1 --> m = { [[o1,o19],F(o1,o19)]
  where o1 is Element of C1, o19 is Element of C1: P[o1,o19] }
  by A3,A5;
A8: P[o,o9];
  Morph-Map(C1 --> m,o,o9) = (the MorphMap of C1 --> m).(o,o9)
    .= F(o,o9) from ValOnPair(A7,A8);
  hence Morph-Map(C1 --> m,o,o9).f = (<^o,o9^> --> m).f by ALTCAT_1:def 1
    .= m by A2,FUNCOP_1:7;
end;

registration
  cluster with_units -> reflexive for non empty AltCatStr;
  coherence;
end;

registration
  let C1,C2 be with_units non empty AltCatStr;
  let o2 be Object of C2;
  cluster C1 --> idm o2 -> id-preserving;
  coherence
  proof
    let o1 be Object of C1;
A1: <^o2,o2^> <> {} by ALTCAT_2:def 7;
    <^o1,o1^> <> {} by ALTCAT_2:def 7;
    hence Morph-Map(C1 --> idm o2,o1,o1).idm o1 = idm o2 by A1,Th24
      .= idm(C1 --> idm o2).o1 by A1,Th21;
  end;
end;

registration
  let C1 be non empty AltGraph;
  let C2 be non empty reflexive AltGraph;
  let o2 be Object of C2;
  let m be Morphism of o2,o2;
  cluster C1 --> m -> reflexive;
  coherence
  proof
    let o be Object of C1;
A1: [o,o] in [:the carrier of C1,the carrier of C1:] by ZFMISC_1:87;
    <^o2,o2^> <> {} by ALTCAT_2:def 7;
    then
A2: (the ObjectMap of C1 --> m).(o,o)
    = ([:the carrier of C1,the carrier of C1:] --> [o2,o2]).[o,o] by Def17
      .= [o2,o2] by A1,FUNCOP_1:7;
    thus thesis by A2;
  end;
end;

registration
  let C1 be non empty AltGraph;
  let C2 be non empty reflexive AltGraph;
  cluster feasible reflexive for FunctorStr over C1,C2;
  existence
  proof set o2 = the Object of C2,m = the Morphism of o2,o2;
    take C1 --> m;
    thus thesis;
  end;
end;

registration
  let C1,C2 be with_units non empty AltCatStr;
  cluster id-preserving feasible reflexive strict for FunctorStr over C1,C2;
  existence
  proof set o2 = the Object of C2;
    take C1 --> idm o2;
    thus thesis;
  end;
end;

definition
  let C1,C2 be non empty AltCatStr;
  let F be FunctorStr over C1,C2;
  attr F is comp-preserving means

  for o1,o2,o3 being Object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {}
  for f being Morphism of o1,o2, g being Morphism of o2,o3
  ex f9 being Morphism of F.o1,F.o2, g9 being Morphism of F.o2,F.o3 st
  f9 = Morph-Map(F,o1,o2).f & g9 = Morph-Map(F,o2,o3).g &
  Morph-Map(F,o1,o3).(g*f) = g9*f9;
end;

definition
  let C1,C2 be non empty AltCatStr;
  let F be FunctorStr over C1,C2;
  attr F is comp-reversing means

  for o1,o2,o3 being Object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {}
  for f being Morphism of o1,o2, g being Morphism of o2,o3
  ex f9 being Morphism of F.o2,F.o1, g9 being Morphism of F.o3,F.o2 st
  f9 = Morph-Map(F,o1,o2).f & g9 = Morph-Map(F,o2,o3).g &
  Morph-Map(F,o1,o3).(g*f) = f9*g9;
end;

definition
  let C1 be non empty transitive AltCatStr;
  let C2 be non empty reflexive AltCatStr;
  let F be Covariant feasible FunctorStr over C1,C2;
  redefine attr F is comp-preserving means
  for o1,o2,o3 being Object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {}
  for f being Morphism of o1,o2, g being Morphism of o2,o3
  holds F.(g*f) = (F.g)*(F.f);
  compatibility
  proof
    hereby
      assume
A1:   F is comp-preserving;
      let o1,o2,o3 be Object of C1 such that
A2:   <^o1,o2^> <> {} and
A3:   <^o2,o3^> <> {};
      let f be Morphism of o1,o2, g be Morphism of o2,o3;
      consider f9 being Morphism of F.o1,F.o2, g9 being Morphism of F.o2,F.o3
      such that
A4:   f9 = Morph-Map(F,o1,o2).f and
A5:   g9 = Morph-Map(F,o2,o3).g and
A6:   Morph-Map(F,o1,o3).(g*f) = g9*f9 by A1,A2,A3;
A7:   <^F.o1,F.o2^> <> {} by A2,Def18;
A8:   <^F.o2,F.o3^> <> {} by A3,Def18;
A9:   f9 = F.f by A2,A4,A7,Def15;
A10:  g9 = F.g by A3,A5,A8,Def15;
A11:  <^o1,o3^> <> {} by A2,A3,ALTCAT_1:def 2;
      then <^F.o1,F.o3^> <> {} by Def18;
      hence F.(g*f) = (F.g)*(F.f) by A6,A9,A10,A11,Def15;
    end;
    assume
A12: for o1,o2,o3 being Object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {}
    for f being Morphism of o1,o2, g being Morphism of o2,o3
    holds F.(g*f) = (F.g)*(F.f);
    let o1,o2,o3 be Object of C1 such that
A13: <^o1,o2^> <> {} and
A14: <^o2,o3^> <> {};
    let f be Morphism of o1,o2, g be Morphism of o2,o3;
A15: <^F.o1,F.o2^> <> {} by A13,Def18;
    then reconsider f9 = Morph-Map(F,o1,o2).f as Morphism of F.o1,F.o2
    by A13,FUNCT_2:5;
A16: <^F.o2,F.o3^> <> {} by A14,Def18;
    then reconsider g9 = Morph-Map(F,o2,o3).g as Morphism of F.o2,F.o3
    by A14,FUNCT_2:5;
    take f9, g9;
    thus f9 = Morph-Map(F,o1,o2).f & g9 = Morph-Map(F,o2,o3).g;
A17: f9 = F.f by A13,A15,Def15;
A18: g9 = F.g by A14,A16,Def15;
A19: <^o1,o3^> <> {} by A13,A14,ALTCAT_1:def 2;
    then <^F.o1,F.o3^> <> {} by Def18;
    hence Morph-Map(F,o1,o3).(g*f) = F.(g*f) by A19,Def15
      .= g9*f9 by A12,A13,A14,A17,A18;
  end;
end;

definition
  let C1 be non empty transitive AltCatStr;
  let C2 be non empty reflexive AltCatStr;
  let F be Contravariant feasible FunctorStr over C1,C2;
  redefine attr F is comp-reversing means
  for o1,o2,o3 being Object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {}
  for f being Morphism of o1,o2, g being Morphism of o2,o3
  holds F.(g*f) = (F.f)*(F.g);
  compatibility
  proof
    hereby
      assume
A1:   F is comp-reversing;
      let o1,o2,o3 be Object of C1 such that
A2:   <^o1,o2^> <> {} and
A3:   <^o2,o3^> <> {};
      let f be Morphism of o1,o2, g be Morphism of o2,o3;
      consider f9 being Morphism of F.o2,F.o1, g9 being Morphism of F.o3,F.o2
      such that
A4:   f9 = Morph-Map(F,o1,o2).f and
A5:   g9 = Morph-Map(F,o2,o3).g and
A6:   Morph-Map(F,o1,o3).(g*f) = f9*g9 by A1,A2,A3;
A7:   <^F.o2,F.o1^> <> {} by A2,Def19;
A8:   <^F.o3,F.o2^> <> {} by A3,Def19;
A9:   f9 = F.f by A2,A4,A7,Def16;
A10:  g9 = F.g by A3,A5,A8,Def16;
A11:  <^o1,o3^> <> {} by A2,A3,ALTCAT_1:def 2;
      then <^F.o3,F.o1^> <> {} by Def19;
      hence F.(g*f) = (F.f)*(F.g) by A6,A9,A10,A11,Def16;
    end;
    assume
A12: for o1,o2,o3 being Object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {}
    for f being Morphism of o1,o2, g being Morphism of o2,o3
    holds F.(g*f) = (F.f)*(F.g);
    let o1,o2,o3 be Object of C1 such that
A13: <^o1,o2^> <> {} and
A14: <^o2,o3^> <> {};
    let f be Morphism of o1,o2, g be Morphism of o2,o3;
A15: <^F.o2,F.o1^> <> {} by A13,Def19;
    then reconsider f9 = Morph-Map(F,o1,o2).f as Morphism of F.o2,F.o1
    by A13,FUNCT_2:5;
A16: <^F.o3,F.o2^> <> {} by A14,Def19;
    then reconsider g9 = Morph-Map(F,o2,o3).g as Morphism of F.o3,F.o2
    by A14,FUNCT_2:5;
    take f9, g9;
    thus f9 = Morph-Map(F,o1,o2).f & g9 = Morph-Map(F,o2,o3).g;
A17: f9 = F.f by A13,A15,Def16;
A18: g9 = F.g by A14,A16,Def16;
A19: <^o1,o3^> <> {} by A13,A14,ALTCAT_1:def 2;
    then <^F.o3,F.o1^> <> {} by Def19;
    hence Morph-Map(F,o1,o3).(g*f) = F.(g*f) by A19,Def16
      .= f9*g9 by A12,A13,A14,A17,A18;
  end;
end;

theorem Th25:
  for C1 being non empty AltGraph, C2 being non empty reflexive AltGraph,
  o2 being Object of C2, m be Morphism of o2,o2,
  F being Covariant feasible FunctorStr over C1,C2 st F = C1 --> m
  for o,o9 being Object of C1, f being Morphism of o,o9 st <^o,o9^> <> {}
  holds F.f = m
proof
  let C1 be non empty AltGraph, C2 be non empty reflexive AltGraph,
  o2 be Object of C2;
A1: <^o2,o2^> <> {} by ALTCAT_2:def 7;
  let m be Morphism of o2,o2,
  F be Covariant feasible FunctorStr over C1,C2 such that
A2: F = C1 --> m;
  let o,o9 be Object of C1, f be Morphism of o,o9;
  assume
A3: <^o,o9^> <> {};
  then <^F.o,F.o9^> <> {} by Def18;
  hence F.f = Morph-Map(F,o,o9).f by A3,Def15
    .= m by A1,A2,A3,Th24;
end;

theorem Th26:
  for C1 being non empty AltGraph, C2 being non empty reflexive AltGraph,
  o2 being Object of C2, m be Morphism of o2,o2,
  o,o9 being Object of C1, f being Morphism of o,o9 st <^o,o9^> <> {}
  holds (C1 --> m).f = m
proof
  let C1 be non empty AltGraph, C2 be non empty reflexive AltGraph,
  o2 be Object of C2;
A1: <^o2,o2^> <> {} by ALTCAT_2:def 7;
  let m be Morphism of o2,o2;
  set F = C1 --> m;
  let o,o9 be Object of C1, f be Morphism of o,o9;
  assume
A2: <^o,o9^> <> {};
  then <^F.o9,F.o^> <> {} by Def19;
  hence F.f = Morph-Map(F,o,o9).f by A2,Def16
    .= m by A1,A2,Th24;
end;

registration
  let C1 be non empty transitive AltCatStr,
  C2 be with_units non empty AltCatStr;
  let o be Object of C2;
  cluster C1 --> idm o -> comp-preserving comp-reversing;
  coherence
  proof
    set F = C1 --> idm o;
    reconsider G = F as Covariant feasible FunctorStr over C1,C2;
A1: <^o,o^> <> {} by ALTCAT_2:def 7;
    G is comp-preserving
    proof
      let o1,o2,o3 be Object of C1;
      assume that
A2:   <^o1,o2^> <> {} and
A3:   <^o2,o3^> <> {};
A4:   <^o1,o3^> <> {} by A2,A3,ALTCAT_1:def 2;
      let f be Morphism of o1,o2, g be Morphism of o2,o3;
A5:   G.g = idm o by A3,Th25;
A6:   G.f = idm o by A2,Th25;
A7:   G.o1 = o by A1,Th21;
A8:   G.o2 = o by A1,Th21;
A9:   G.o3 = o by A1,Th21;
      thus G.(g*f) = idm o by A4,Th25
        .= (G.g)*(G.f) by A1,A5,A6,A7,A8,A9,ALTCAT_1:20;
    end;
    hence F is comp-preserving;
    let o1,o2,o3 be Object of C1;
    assume that
A10: <^o1,o2^> <> {} and
A11: <^o2,o3^> <> {};
A12: <^o1,o3^> <> {} by A10,A11,ALTCAT_1:def 2;
    let f be Morphism of o1,o2, g be Morphism of o2,o3;
A13: F.g = idm o by A11,Th26;
A14: F.f = idm o by A10,Th26;
A15: F.o1 = o by A1,Th21;
A16: F.o2 = o by A1,Th21;
A17: F.o3 = o by A1,Th21;
    thus F.(g*f) = idm o by A12,Th26
      .= (F.f)*(F.g) by A1,A13,A14,A15,A16,A17,ALTCAT_1:20;
  end;
end;

definition
  let C1 be transitive with_units non empty AltCatStr,
  C2 be with_units non empty AltCatStr;
  mode Functor of C1,C2 -> FunctorStr over C1,C2 means
    :Def25:
    it is feasible id-preserving &
    (it is Covariant comp-preserving or it is Contravariant comp-reversing);
  existence
  proof set o = the Object of C2;
    take C1 --> idm o;
    thus thesis;
  end;
end;

definition
  let C1 be transitive with_units non empty AltCatStr,
  C2 be with_units non empty AltCatStr, F be Functor of C1,C2;
  attr F is covariant means
  :Def26:
  F is Covariant comp-preserving;
  attr F is contravariant means
  :Def27:
  F is Contravariant comp-reversing;
end;

definition
  let A be AltCatStr, B be SubCatStr of A;
  func incl B -> strict FunctorStr over B,A means
  :Def28:
  the ObjectMap of it = id [:the carrier of B, the carrier of B:] &
  the MorphMap of it = id the Arrows of B;
  existence
  proof
    the carrier of B c= the carrier of A by ALTCAT_2:def 11;
    then reconsider CC = [:the carrier of B, the carrier of B:]
    as Subset of [:the carrier of A, the carrier of A:] by ZFMISC_1:96;
    set OM = id [:the carrier of B, the carrier of B:];
    OM = incl CC;
    then reconsider OM as bifunction of the carrier of B, the carrier of A;
    set MM = id the Arrows of B;
    MM is MSUnTrans of OM, the Arrows of B, the Arrows of A
    proof
      per cases;
      case [:the carrier of A,the carrier of A:] <> {};
        then reconsider I29 = [:the carrier of A,the carrier of A:]
        as non empty set;
        reconsider B9 = the Arrows of A as ManySortedSet of I29;
        reconsider f9 = OM as
        Function of [:the carrier of B,the carrier of B:],I29;
        take I29, B9, f9;
        thus OM = f9 & the Arrows of A = B9;
        thus MM is ManySortedFunction of the Arrows of B,B9*f9
        proof
          let i be object;
          assume
A1:       i in [:the carrier of B,the carrier of B:];
          then
          A2:       MM
.i is Function of (the Arrows of B).i, (the Arrows of B).i
          by PBOOLE:def 15;
A3:       the Arrows of B cc= the Arrows of A by ALTCAT_2:def 11;
          (B9*f9).i = B9.(f9.i) by A1,FUNCT_2:15
            .= (the Arrows of A).i by A1,FUNCT_1:18;
          then (the Arrows of B).i c= (B9*f9).i by A1,A3,ALTCAT_2:def 2;
          hence thesis by A2,FUNCT_2:7;
        end;
      end;
      case [:the carrier of A,the carrier of A:] = {};
        then CC = {};
        hence thesis;
      end;
    end;
    then reconsider MM as MSUnTrans of OM, the Arrows of B, the Arrows of A;
    take FunctorStr(#OM,MM#);
    thus thesis;
  end;
  correctness;
end;

definition
  let A be AltGraph;
  func id A -> strict FunctorStr over A,A means
  :Def29:
  the ObjectMap of it = id [:the carrier of A, the carrier of A:] &
  the MorphMap of it = id the Arrows of A;
  existence
  proof
    reconsider OM = id [:the carrier of A, the carrier of A:]
    as bifunction of the carrier of A, the carrier of A;
    set MM = id the Arrows of A;
    MM is MSUnTrans of OM, the Arrows of A, the Arrows of A
    proof
      per cases;
      case [:the carrier of A,the carrier of A:] <> {};
        then reconsider I29 = [:the carrier of A,the carrier of A:]
        as non empty set;
        reconsider A9 = the Arrows of A as ManySortedSet of I29;
        reconsider f9 = OM as
        Function of [:the carrier of A,the carrier of A:],I29;
        take I29, A9, f9;
        thus OM = f9 & the Arrows of A = A9;
        thus MM is ManySortedFunction of the Arrows of A,A9*f9
        proof
          let i be object;
          assume
A1:       i in [:the carrier of A,the carrier of A:];
          then (A9*f9).i = A9.(f9.i) by FUNCT_2:15
            .= (the Arrows of A).i by A1,FUNCT_1:18;
          hence thesis by A1,PBOOLE:def 15;
        end;
      end;
      case
        [:the carrier of A,the carrier of A:] = {};
        hence thesis;
      end;
    end;
    then reconsider MM as MSUnTrans of OM, the Arrows of A, the Arrows of A;
    take FunctorStr(#OM,MM#);
    thus thesis;
  end;
  correctness;
end;

registration
  let A be AltCatStr, B be SubCatStr of A;
  cluster incl B -> Covariant;
  coherence
  proof
    reconsider b = the carrier of B as Subset of A by ALTCAT_2:def 11;
    incl b = id b;
    then reconsider f = id the carrier of B as
    Function of the carrier of B, the carrier of A;
    take f;
    thus
    the ObjectMap of incl B = id[:the carrier of B,the carrier of B:] by Def28
      .= [:f,f:] by FUNCT_3:69;
  end;
end;

theorem Th27:
  for A being non empty AltCatStr, B being non empty SubCatStr of A,
  o being Object of B holds (incl B).o = o
proof
  let A be non empty AltCatStr, B be non empty SubCatStr of A,
  o be Object of B;
A1: [o,o] in [:the carrier of B,the carrier of B:] by ZFMISC_1:87;
  thus
  (incl B).o = ((id[:the carrier of B,the carrier of B:]).[o,o])`1 by Def28
    .= [o,o]`1 by A1,FUNCT_1:18
    .= o;
end;

theorem Th28:
  for A being non empty AltCatStr, B being non empty SubCatStr of A,
  o1,o2 being Object of B holds <^o1,o2^> c= <^(incl B).o1,(incl B).o2^>
proof
  let A be non empty AltCatStr, B be non empty SubCatStr of A,
  o1,o2 be Object of B;
A1: [o1,o2] in [:the carrier of B,the carrier of B:] by ZFMISC_1:87;
A2: <^o1,o2^> = (the Arrows of B).(o1,o2) by ALTCAT_1:def 1
    .= (the Arrows of B).[o1,o2];
A3: (incl B).o1 = o1 by Th27;
  (incl B).o2 = o2 by Th27;
  then
A4: <^(incl B).o1,(incl B).o2^> = (the Arrows of A).(o1,o2) by A3,
ALTCAT_1:def 1
    .= (the Arrows of A).[o1,o2];
  the Arrows of B cc= the Arrows of A by ALTCAT_2:def 11;
  hence thesis by A1,A2,A4,ALTCAT_2:def 2;
end;

registration
  let A be non empty AltCatStr, B be non empty SubCatStr of A;
  cluster incl B -> feasible;
  coherence
  by Th28,XBOOLE_1:3;
end;

definition
  let A,B be AltGraph, F be FunctorStr over A,B;
  attr F is faithful means

  the MorphMap of F is "1-1";
end;

definition
  let A,B be AltGraph, F be FunctorStr over A,B;
  attr F is full means

  ex B9 being ManySortedSet of [:the carrier of A, the carrier of A:],
  f being ManySortedFunction of (the Arrows of A),B9 st
  B9 = (the Arrows of B)*the ObjectMap of F & f = the MorphMap of F
  & f is "onto";
end;

definition
  let A be AltGraph, B be non empty AltGraph, F be FunctorStr over A,B;
  redefine attr F is full means
  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";
  compatibility;
end;

definition
  let A,B be AltGraph, F be FunctorStr over A,B;
  attr F is injective means

  F is one-to-one faithful;
  attr F is surjective means

  F is full onto;
end;

definition
  let A,B be AltGraph, F be FunctorStr over A,B;
  attr F is bijective means

  F is injective surjective;
end;

registration
  let A,B be transitive with_units non empty AltCatStr;
  cluster strict covariant contravariant feasible for Functor of A,B;
  existence
  proof set o = the Object of B;
    reconsider F = A --> idm o as Functor of A,B by Def25;
    take F;
    thus thesis;
  end;
end;

theorem Th29:
  for A being non empty AltGraph, o being Object of A holds (id A).o = o
proof
  let A be non empty AltGraph, o be Object of A;
A1: [o,o] in [:the carrier of A,the carrier of A:] by ZFMISC_1:87;
  thus (id A).o = ((id[:the carrier of A,the carrier of A:]).[o,o])`1 by Def29
    .= ([o,o])`1 by A1,FUNCT_1:18
    .= o;
end;

theorem Th30:
  for A being non empty AltGraph, o1,o2 being Object of A st <^o1,o2^> <> {}
  for m being Morphism of o1,o2 holds Morph-Map(id A,o1,o2).m = m
proof
  let A be non empty AltGraph, o1,o2 be Object of A such that
 <^o1,o2^> <> {};
  let m be Morphism of o1,o2;
A1: [o1,o2] in [:the carrier of A, the carrier of A:] by ZFMISC_1:87;
  Morph-Map(id A,o1,o2) = (id the Arrows of A).[o1,o2] by Def29;
  hence Morph-Map(id A,o1,o2).m
  = (id((the Arrows of A).(o1,o2))).m by A1,MSUALG_3:def 1
    .= (id<^o1,o2^>).m by ALTCAT_1:def 1
    .= m;
end;

registration
  let A be non empty AltGraph;
  cluster id A -> feasible Covariant;
  coherence
  proof
    thus id A is feasible
    proof
      let o1,o2 be Object of A;
A1:   [o1,o2] in [:the carrier of A, the carrier of A:] by ZFMISC_1:87;
      (the ObjectMap of id A).(o1,o2)
      = (id[:the carrier of A, the carrier of A:]).[o1,o2] by Def29
        .= [o1,o2] by A1,FUNCT_1:18;
      then (the Arrows of A).((the ObjectMap of id A).(o1,o2))
      = (the Arrows of A).(o1,o2)
        .= <^o1,o2^> by ALTCAT_1:def 1;
      hence thesis;
    end;
    thus id A is Covariant
    proof
      take I = id the carrier of A;
      thus
      the ObjectMap of id A = id[:the carrier of A,the carrier of A:] by Def29
        .= [:I,I:] by FUNCT_3:69;
    end;
  end;
end;

registration
  let A be non empty AltGraph;
  cluster Covariant feasible for FunctorStr over A,A;
  existence
  proof
    take id A;
    thus thesis;
  end;
end;

theorem Th31:
  for A being non empty AltGraph, o1,o2 being Object of A st <^o1,o2^> <> {}
  for F being Covariant feasible FunctorStr over A,A st F = id A
  for m being Morphism of o1,o2 holds F.m = m
proof
  let A be non empty AltGraph, o1,o2 be Object of A such that
A1: <^o1,o2^> <> {};
  let F be Covariant feasible FunctorStr over A,A such that
A2: F = id A;
  let m be Morphism of o1,o2;
  <^F.o1,F.o2^> <> {} by A1,Def18;
  hence F.m = Morph-Map(F,o1,o2).m by A1,Def15
    .= m by A1,A2,Th30;
end;

registration
  let A be transitive with_units non empty AltCatStr;
  cluster id A -> id-preserving comp-preserving;
  coherence
  proof
    thus id A is id-preserving
    proof
      let o be Object of A;
      <^o,o^> <> {} by ALTCAT_2:def 7;
      hence Morph-Map(id A,o,o).idm o = idm o by Th30
        .= idm (id A).o by Th29;
    end;
    set F = id A;
    F is comp-preserving
    proof
      let o1,o2,o3 be Object of A such that
A1:   <^o1,o2^> <> {} and
A2:   <^o2,o3^> <> {};
      let f be Morphism of o1,o2, g be Morphism of o2,o3;
A3:   <^o1,o3^> <> {} by A1,A2,ALTCAT_1:def 2;
A4:   F.o1 = o1 by Th29;
A5:   F.o2 = o2 by Th29;
A6:   F.o3 = o3 by Th29;
A7:   F.g = g by A2,Th31;
      F.f = f by A1,Th31;
      hence thesis by A3,A4,A5,A6,A7,Th31;
    end;
    hence thesis;
  end;
end;

definition
  let A be transitive with_units non empty AltCatStr;
  redefine func id A -> strict covariant Functor of A,A;
  coherence by Def25,Def26;
end;

registration
  let A be AltGraph;
  cluster id A -> bijective;
  coherence
  proof
    set CC=[:the carrier of A,the carrier of A:];
A1: the ObjectMap of id A = id CC by Def29;
    hence id A is one-to-one;
    thus id A is faithful
    proof
      per cases;
      suppose
A2:     the carrier of A <> {};
        let i be set, f be Function such that
A3:     i in dom(the MorphMap of id A) and
A4:     (the MorphMap of id A).i = f;
        consider o1,o2 being Element of A such that
A5:     i = [o1,o2] by A2,A3,DOMAIN_1:1;
        reconsider o1,o2 as Object of A;
A6:     [o1,o2] in [:the carrier of A, the carrier of A:] by A2,ZFMISC_1:87;
        f = (id the Arrows of A).(o1,o2) by A4,A5,Def29
          .= id((the Arrows of A).[o1,o2]) by A6,MSUALG_3:def 1;
        hence thesis;
      end;
      suppose
A7:     the carrier of A = {};
        let i be set, f be Function such that
A8:     i in dom(the MorphMap of id A) and
        (the MorphMap of id A).i = f;
        dom(the MorphMap of id A)
        = [:the carrier of A, the carrier of A:] by PARTFUN1:def 2
          .= {} by A7,ZFMISC_1:90;
        hence thesis by A8;
      end;
    end;
    thus id A is full proof per cases;
      suppose A is non empty;
        then reconsider A as non empty AltGraph;
        id A is full
        proof
          reconsider f = the MorphMap of id A as
          ManySortedFunction of (the Arrows of A),
          (the Arrows of A)*the ObjectMap of id A by Def4;
          take f;
          thus f = the MorphMap of id A;
          let i be set;
          assume
A9:       i in [:the carrier of A,the carrier of A:];
          then consider o1,o2 being Element of A such that
A10:      i = [o1,o2] by DOMAIN_1:1;
          reconsider o1,o2 as Object of A;
A11:      [o1,o2] in [:the carrier of A, the carrier of A:] by ZFMISC_1:87;
A12:      dom(the ObjectMap of id A) = CC by A1;
          f.i = (id the Arrows of A).(o1,o2) by A10,Def29
            .= id((the Arrows of A).[o1,o2]) by A11,MSUALG_3:def 1;
          hence rng(f.i) = (the Arrows of A).[o1,o2]
.= (the Arrows of A).((the ObjectMap of id A).i) by A1,A9,A10,FUNCT_1:18
.= ((the Arrows of A)*the ObjectMap of id A).i by A9,A12,FUNCT_1:13;
        end;
        hence thesis;
      end;
      suppose A is empty;
        then
A13:    the carrier of A = {};
the ObjectMap of id A = id [:the carrier of A, the carrier of A:] by Def29;
        then reconsider B = (the Arrows of A)*the ObjectMap of id A as
        ManySortedSet of [:the carrier of A, the carrier of A:] by Th2;
        reconsider f = the MorphMap of id A as
        ManySortedSet of [:the carrier of A, the carrier of A:];
        f is ManySortedFunction of (the Arrows of A),B
        proof
          let i be object;
          thus thesis by A13,ZFMISC_1:90;
        end;
        then reconsider f as ManySortedFunction of (the Arrows of A),B;
        take B,f;
        thus
        B = (the Arrows of A)*the ObjectMap of id A & f = the MorphMap of id A;
        let i be set;
        thus thesis by A13,ZFMISC_1:90;
      end;
    end;
    the ObjectMap of id A is onto by A1;
    hence id A is onto;
  end;
end;

begin :: The composition of functors

definition
  let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph;
  let F be feasible FunctorStr over C1,C2, G be FunctorStr over C2,C3;
  func G*F -> strict FunctorStr over C1,C3 means
  :Def36:
  the ObjectMap of it = (the ObjectMap of G)*the ObjectMap of F &
  the MorphMap of it =
  ((the MorphMap of G)*the ObjectMap of F)**the MorphMap of F;
  existence
  proof
    reconsider O = (the ObjectMap of G)*the ObjectMap of F
    as bifunction of the carrier of C1, the carrier of C3;
    set I1 = [:the carrier of C1,the carrier of C1:];
    reconsider H = (the MorphMap of G)*the ObjectMap of F
    as MSUnTrans of O,(the Arrows of C2)*the ObjectMap of F,the Arrows of C3
    by Th17;
    for ii being set st ii in I1 &
    ((the Arrows of C2)*the ObjectMap of F).ii = {}
    holds (the Arrows of C1).ii = {} or ((the Arrows of C3)*O).ii = {}
    proof
      let ii be set such that
A1:   ii in I1 and
A2:   ((the Arrows of C2)*the ObjectMap of F).ii = {};
A3:   dom the ObjectMap of F = I1 by FUNCT_2:def 1;
      reconsider o1 = ii`1, o2 = ii`2 as Object of C1 by A1,MCART_1:10;
      ii = [o1,o2] by A1,MCART_1:21;
      then
A4:   (the Arrows of C2).((the ObjectMap of F).(o1,o2))
      = {} by A1,A2,A3,FUNCT_1:13;
      (the Arrows of C1).ii = (the Arrows of C1).(o1,o2) by A1,MCART_1:21
        .= <^o1,o2^> by ALTCAT_1:def 1
        .= {} by A4,Def11;
      hence thesis;
    end;
    then reconsider M = H**the MorphMap of F
    as MSUnTrans of O, the Arrows of C1, the Arrows of C3 by Th19;
    take FunctorStr(#O,M#);
    thus thesis;
  end;
  correctness;
end;

registration
  let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph;
  let F be Covariant feasible FunctorStr over C1,C2,
  G be Covariant FunctorStr over C2,C3;
  cluster G*F -> Covariant;
  correctness
  proof
    the ObjectMap of F is Covariant by Def12;
    then consider f being Function of the carrier of C1, the carrier of C2
    such that
A1: the ObjectMap of F = [:f,f:];
    the ObjectMap of G is Covariant by Def12;
    then consider g being Function of the carrier of C2, the carrier of C3
    such that
A2: the ObjectMap of G = [:g,g:];
    take g*f;
    thus
    the ObjectMap of G*F = (the ObjectMap of G)*the ObjectMap of F by Def36
      .= [:g*f,g*f:] by A1,A2,FUNCT_3:71;
  end;
end;

registration
  let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph;
  let F be Contravariant feasible FunctorStr over C1,C2,
  G be Covariant FunctorStr over C2,C3;
  cluster G*F -> Contravariant;
  correctness
  proof
    the ObjectMap of F is Contravariant by Def13;
    then consider f being Function of the carrier of C1, the carrier of C2
    such that
A1: the ObjectMap of F = ~[:f,f:];
    the ObjectMap of G is Covariant by Def12;
    then consider g being Function of the carrier of C2, the carrier of C3
    such that
A2: the ObjectMap of G = [:g,g:];
    take g*f;
    thus
    the ObjectMap of G*F = (the ObjectMap of G)*the ObjectMap of F by Def36
      .= ~([:g,g:]*[:f,f:]) by A1,A2,ALTCAT_2:2
      .= ~[:g*f,g*f:] by FUNCT_3:71;
  end;
end;

registration
  let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph;
  let F be Covariant feasible FunctorStr over C1,C2,
  G be Contravariant FunctorStr over C2,C3;
  cluster G*F -> Contravariant;
  correctness
  proof
    the ObjectMap of F is Covariant by Def12;
    then consider f being Function of the carrier of C1, the carrier of C2
    such that
A1: the ObjectMap of F = [:f,f:];
    the ObjectMap of G is Contravariant by Def13;
    then consider g being Function of the carrier of C2, the carrier of C3
    such that
A2: the ObjectMap of G = ~[:g,g:];
    take g*f;
    thus
    the ObjectMap of G*F = (the ObjectMap of G)*the ObjectMap of F by Def36
      .= ~([:g,g:]*[:f,f:]) by A1,A2,ALTCAT_2:3
      .= ~[:g*f,g*f:] by FUNCT_3:71;
  end;
end;

registration
  let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph;
  let F be Contravariant feasible FunctorStr over C1,C2,
  G be Contravariant FunctorStr over C2,C3;
  cluster G*F -> Covariant;
  correctness
  proof
    the ObjectMap of F is Contravariant by Def13;
    then consider f being Function of the carrier of C1, the carrier of C2
    such that
A1: the ObjectMap of F = ~[:f,f:];
    the ObjectMap of G is Contravariant by Def13;
    then consider g being Function of the carrier of C2, the carrier of C3
    such that
A2: the ObjectMap of G = ~[:g,g:];
    take g*f;
    thus
    the ObjectMap of G*F = (the ObjectMap of G)*the ObjectMap of F by Def36
      .= ~(~[:g,g:]*[:f,f:]) by A1,A2,ALTCAT_2:2
      .= ~~([:g,g:]*[:f,f:]) by ALTCAT_2:3
      .= [:g,g:]*[:f,f:] by FUNCT_4:53
      .= [:g*f,g*f:] by FUNCT_3:71;
  end;
end;

registration
  let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph;
  let F be feasible FunctorStr over C1,C2,
  G be feasible FunctorStr over C2,C3;
  cluster G*F -> feasible;
  coherence
  proof
    let o1,o2 be Object of C1 such that
A1: <^o1,o2^> <> {};
    reconsider p1 = ((the ObjectMap of F).(o1,o2))`1,
    p2 = ((the ObjectMap of F).(o1,o2))`2 as Element of C2 by MCART_1:10;
    reconsider p1,p2 as Object of C2;
    [o1,o2] in [:the carrier of C1,the carrier of C1:] by ZFMISC_1:87;
    then
A2: [o1,o2] in dom the ObjectMap of F by FUNCT_2:def 1;
A3: ((the ObjectMap of F).(o1,o2)) = [p1,p2] by MCART_1:21;
A4: ((the ObjectMap of(G*F)).(o1,o2))
    = ((the ObjectMap of G)*the ObjectMap of F).[o1,o2] by Def36
      .= (the ObjectMap of G).(p1,p2) by A2,A3,FUNCT_1:13;
    <^p1,p2^> = (the Arrows of C2).(p1,p2) by ALTCAT_1:def 1
      .= (the Arrows of C2).((the ObjectMap of F).(o1,o2)) by MCART_1:21;
    then <^p1,p2^> <> {} by A1,Def11;
    hence thesis by A4,Def11;
  end;
end;

theorem
  for C1 being non empty AltGraph, C2,C3,C4 being non empty reflexive AltGraph,
  F being feasible FunctorStr over C1,C2,
  G being feasible FunctorStr over C2,C3, H being FunctorStr over C3,C4
  holds H*G*F = H*(G*F)
proof
  let C1 be non empty AltGraph, C2,C3,C4 be non empty reflexive AltGraph,
  F be feasible FunctorStr over C1,C2,
  G be feasible FunctorStr over C2,C3, H be FunctorStr over C3,C4;
A1: the ObjectMap of H*G*F = (the ObjectMap of H*G)*the ObjectMap of F by Def36
    .= (the ObjectMap of H)*(the ObjectMap of G)*the ObjectMap of F by Def36
    .= (the ObjectMap of H)*((the ObjectMap of G)*the ObjectMap of F)
  by RELAT_1:36
    .= (the ObjectMap of H)*the ObjectMap of(G*F) by Def36
    .= the ObjectMap of H*(G*F) by Def36;
  the MorphMap of H*G*F
  = ((the MorphMap of H*G)*the ObjectMap of F)**the MorphMap of F by Def36
    .= ((the MorphMap of H)*(the ObjectMap of G)**the MorphMap of G)
  *(the ObjectMap of F)**the MorphMap of F by Def36
    .= (the MorphMap of H)*(the ObjectMap of G)*(the ObjectMap of F)
  **((the MorphMap of G)*the ObjectMap of F)**the MorphMap of F by Th12
    .= (the MorphMap of H)*((the ObjectMap of G)*the ObjectMap of F)
  **((the MorphMap of G)*the ObjectMap of F)**the MorphMap of F by RELAT_1:36
    .= ((the MorphMap of H)*the ObjectMap of G*F)**
  ((the MorphMap of G)*the ObjectMap of F)**the MorphMap of F by Def36
    .= ((the MorphMap of H)*the ObjectMap of G*F)**
  (((the MorphMap of G)*the ObjectMap of F)**the MorphMap of F) by PBOOLE:140
    .= ((the MorphMap of H)*the ObjectMap of G*F)**the MorphMap of G*F by Def36
    .= the MorphMap of H*(G*F) by Def36;
  hence thesis by A1;
end;

theorem Th33:
  for C1 being non empty AltCatStr, C2,C3 being non empty reflexive AltCatStr,
  F be feasible reflexive FunctorStr over C1,C2, G be FunctorStr over C2,C3,
  o be Object of C1 holds (G*F).o = G.(F.o)
proof
  let C1 be non empty AltCatStr, C2,C3 be non empty reflexive AltCatStr,
  F be feasible reflexive FunctorStr over C1,C2, G be FunctorStr over C2,C3,
  o be Object of C1;
  dom the ObjectMap of F = [:the carrier of C1,the carrier of C1:]
  by FUNCT_2:def 1;
  then
A1: [o,o] in dom the ObjectMap of F by ZFMISC_1:87;
  thus (G*F).o = (((the ObjectMap of G)*the ObjectMap of F).(o,o))`1 by Def36
    .= ((the ObjectMap of G).((the ObjectMap of F).[o,o]))`1 by A1,FUNCT_1:13
    .= G.(F.o) by Def10;
end;

theorem Th34:
  for C1 being non empty AltGraph, C2,C3 being non empty reflexive AltGraph,
  F be feasible reflexive FunctorStr over C1,C2, G be FunctorStr over C2,C3,
  o be Object of C1
  holds Morph-Map(G*F,o,o) = Morph-Map(G,F.o,F.o)*Morph-Map(F,o,o)
proof
  let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph,
  F be feasible reflexive FunctorStr over C1,C2,
  G be FunctorStr over C2,C3, o be Object of C1;
A1: dom(the MorphMap of G) = [:the carrier of C2,the carrier of C2:]
  by PARTFUN1:def 2;
  rng(the ObjectMap of F) c= [:the carrier of C2,the carrier of C2:];
  then dom((the MorphMap of G)*the ObjectMap of F)
  = dom(the ObjectMap of F) by A1,RELAT_1:27
    .= [:the carrier of C1,the carrier of C1:] by FUNCT_2:def 1;
  then
A2: [o,o] in dom((the MorphMap of G)*the ObjectMap of F) by ZFMISC_1:87;
  dom(the MorphMap of F) = [:the carrier of C1,the carrier of C1:]
  by PARTFUN1:def 2;
  then [o,o] in dom(the MorphMap of F) by ZFMISC_1:87;
  then [o,o] in dom((the MorphMap of G)*the ObjectMap of F)
  /\ dom(the MorphMap of F) by A2,XBOOLE_0:def 4;
  then
  A3: [o,o] in dom(((the MorphMap of G)*the ObjectMap of F)**the MorphMap of F)
  by PBOOLE:def 19;
A4: ((the MorphMap of G)*the ObjectMap of F).[o,o]
  = (the MorphMap of G).((the ObjectMap of F).(o,o)) by A2,FUNCT_1:12
    .= Morph-Map(G,F.o,F.o) by Def10;
  thus Morph-Map(G*F,o,o)
  = (((the MorphMap of G)*the ObjectMap of F)**the MorphMap of F).(o,o)
  by Def36
    .= Morph-Map(G,F.o,F.o)*Morph-Map(F,o,o) by A3,A4,PBOOLE:def 19;
end;

registration
  let C1,C2,C3 be with_units non empty AltCatStr;
  let F be id-preserving feasible reflexive FunctorStr over C1,C2;
  let G be id-preserving FunctorStr over C2,C3;
  cluster G*F -> id-preserving;
  coherence
  proof
    let o be Object of C1;
A1: [o,o] in [:the carrier of C1,the carrier of C1:] by ZFMISC_1:87;
    then [o,o] in dom the ObjectMap of F by FUNCT_2:def 1;
    then ((the Arrows of C2)*the ObjectMap of F).[o,o]
    = (the Arrows of C2).((the ObjectMap of F).(o,o)) by FUNCT_1:13
      .= (the Arrows of C2).(F.o,F.o) by Def10
      .= <^F.o,F.o^> by ALTCAT_1:def 1;
    then
A2: ((the Arrows of C2)*the ObjectMap of F).[o,o] <> {} by ALTCAT_2:def 7;
    the MorphMap of F is ManySortedFunction of the Arrows of C1,
    (the Arrows of C2)*the ObjectMap of F by Def4;
    then Morph-Map(F,o,o) is Function of (the Arrows of C1).[o,o],
    ((the Arrows of C2)*the ObjectMap of F).[o,o] by A1,PBOOLE:def 15;
    then
A3: dom Morph-Map(F,o,o) = (the Arrows of C1).(o,o) by A2,FUNCT_2:def 1
      .= <^o,o^> by ALTCAT_1:def 1;
    thus Morph-Map(G*F,o,o).idm o
    = (Morph-Map(G,F.o,F.o)*Morph-Map(F,o,o)).idm o by Th34
      .= Morph-Map(G,F.o,F.o).(Morph-Map(F,o,o).idm o) by A3,ALTCAT_1:19
,FUNCT_1:13
      .= Morph-Map(G,F.o,F.o).idm F.o by Def20
      .= idm G.(F.o) by Def20
      .= idm (G*F).o by Th33;
  end;
end;

definition
  let A,C be non empty reflexive AltCatStr;
  let B be non empty SubCatStr of A;
  let F be FunctorStr over A,C;
  func F|B -> FunctorStr over B,C equals
  F*incl B;
  correctness;
end;

begin :: The inverse functor

definition
  let A,B be non empty AltGraph, F be FunctorStr over A,B;
  assume
A1: F is bijective;
  func F" -> strict FunctorStr over B,A means
  :Def38:
  the ObjectMap of it = (the ObjectMap of F)" &
  ex f being ManySortedFunction of (the Arrows of A),
  (the Arrows of B)*the ObjectMap of F st
  f = the MorphMap of F & the MorphMap of it = f""*(the ObjectMap of F)";
  existence
  proof
    set OF = the ObjectMap of F;
    F is injective by A1;
    then F is one-to-one;
    then
A2: OF is one-to-one;
    F is surjective by A1;
    then F is onto;
    then OF is onto;
    then
A3: rng OF = [:the carrier of B,the carrier of B:];
    then reconsider OM = (the ObjectMap of F)" as
    bifunction of the carrier of B, the carrier of A by A2,FUNCT_2:25;
    reconsider f = the MorphMap of F as
    ManySortedFunction of (the Arrows of A), (the Arrows of B)*OF by Def4;
    (the Arrows of B)*OF*OM = (the Arrows of B)*(OF*OM) by RELAT_1:36
      .= (the Arrows of B)*id[:the carrier of B,the carrier of B:]
    by A2,A3,FUNCT_2:29
      .= the Arrows of B by Th2;
    then f""*OM is ManySortedFunction of the Arrows of B, (the Arrows of A)*OM
    by ALTCAT_2:5;
    then reconsider MM = f""*OM
    as MSUnTrans of OM, the Arrows of B, the Arrows of A by Def4;
    take G = FunctorStr(#OM,MM#);
    thus the ObjectMap of G = OF";
    take f;
    thus thesis;
  end;
  uniqueness;
end;

theorem Th35:
  for A,B being transitive with_units non empty AltCatStr,
  F being feasible FunctorStr over A,B st F is bijective
  holds F" is bijective feasible
proof
  let A,B be transitive with_units non empty AltCatStr;
  let F be feasible FunctorStr over A,B such that
A1: F is bijective;
  set G = F";
A2: the ObjectMap of G = (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 G is one-to-one by A2;
  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 G = 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:],
  BB = [:the carrier of B,the carrier of B:];
A11: rng the ObjectMap of F = BB by A7;
  reconsider f = the MorphMap of G as ManySortedFunction of
  (the Arrows of B),(the Arrows of A)*the ObjectMap of G by Def4;
  f is "1-1"
  proof
    let i be set, g be Function such that
A12: i in dom f and
A13: f.i = g;
    i in BB 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 AA;
    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 thesis by A16;
  end;
  hence the MorphMap of G is "1-1";
  thus G is full
  proof
    take f;
    thus f = the MorphMap of G;
    let i be set;
    assume
A17: i in BB;
    then
A18: i in dom the ObjectMap of G 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 AA;
    then ((the ObjectMap of G).i) in dom h by A2,PARTFUN1:def 2;
    then
A21: h.((the ObjectMap of G).i) is one-to-one by A5,A8;
    set j = (the ObjectMap of G).i;
A22: h.j is Function of (the Arrows of A).j,
    ((the Arrows of B)*the ObjectMap of F).j by A2,A20,PBOOLE:def 15;
    consider o1,o2 being Element of A such that
A23: j = [o1,o2] by A2,A20,DOMAIN_1:1;
    reconsider o1,o2 as Object of A;
A24: now
      assume (the Arrows of A).j <> {};
      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).j <> {} by A2,A20,A23,
FUNCT_1:13;
    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 G).i)) by A2,A21,FUNCT_1:33
      .= (the Arrows of A).((the ObjectMap of G).i) by A22,A24,FUNCT_2:def 1
      .= ((the Arrows of A)*the ObjectMap of G).i by A18,FUNCT_1:13;
  end;
  thus rng the ObjectMap of G = dom the ObjectMap of F by A2,A4,FUNCT_1:33
    .= AA by FUNCT_2:def 1;
  let o1,o2 be Object of B;
  assume <^o1,o2^> <> {};
  then
A25: (the Arrows of B).(o1,o2) <> {} by ALTCAT_1:def 1;
A26: [o1,o2] in BB by ZFMISC_1:87;
  then consider p1,p2 being Element of A such that
A27: (the ObjectMap of G).[o1,o2] = [p1,p2] by DOMAIN_1:1,FUNCT_2:5;
  reconsider p1,p2 as Object of A;
  [o1,o2] in dom the ObjectMap of G by A26,FUNCT_2:def 1;
  then
A28: (the ObjectMap of F).(p1,p2)
  = ((the ObjectMap of F)*(the ObjectMap of G)).[o1,o2] by A27,FUNCT_1:13
    .= (id BB).[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 G).(o1,o2)) = {};
A30: [p1,p2] in AA 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;
end;

theorem Th36:
  for A,B being transitive with_units non empty AltCatStr,
  F being feasible reflexive FunctorStr over A,B st F is bijective coreflexive
  holds F" is reflexive
proof
  let A,B be transitive with_units non empty AltCatStr,
  F be feasible reflexive FunctorStr over A,B such that
A1: F is bijective and
A2: F is coreflexive;
  set G = F";
A3: the ObjectMap of G = (the ObjectMap of F)" by A1,Def38;
  let o be Object of B;
A4: dom the ObjectMap of F = [:the carrier of A,the carrier of A:]
  by FUNCT_2:def 1;
  consider p being Object of A such that
A5: o = F.p by A2,Th20;
  F is injective by A1;
  then F is one-to-one;
  then
A6: the ObjectMap of F is one-to-one;
A7: [p,p] in dom the ObjectMap of F by A4,ZFMISC_1:87;
A8: G.(F.p) = (G*F).p by Th33
    .= (((the ObjectMap of G)*the ObjectMap of F).(p,p))`1 by Def36
    .= ((id dom the ObjectMap of F).[p,p])`1 by A3,A6,FUNCT_1:39
    .= [p,p]`1 by A7,FUNCT_1:18
    .= p;
  thus (the ObjectMap of G).(o,o)
  = (the ObjectMap of G).((the ObjectMap of F).(p,p)) by A5,Def10
    .= ((the ObjectMap of G)*(the ObjectMap of F)).[p,p] by A7,FUNCT_1:13
    .= (id dom the ObjectMap of F).[p,p] by A3,A6,FUNCT_1:39
    .= [G.o,G.o] by A5,A7,A8,FUNCT_1:18;
end;

theorem Th37:
  for A,B being transitive with_units non empty AltCatStr,
  F being feasible reflexive id-preserving FunctorStr over A,B
  st F is bijective coreflexive holds F" is id-preserving
proof
  let A,B be transitive with_units non empty AltCatStr,
  F be feasible reflexive id-preserving FunctorStr over A,B such that
A1: F is bijective coreflexive;
  set G = F";
  reconsider H = G as feasible reflexive FunctorStr over B,A by A1,Th35,Th36;
A2: the ObjectMap of G = (the ObjectMap of F)" by A1,Def38;
  consider f being ManySortedFunction of (the Arrows of A),
  (the Arrows of B)*the ObjectMap of F such that
A3: f = the MorphMap of F and
A4: the MorphMap of G = f""*(the ObjectMap of F)" by A1,Def38;
  let o be Object of B;
A5: F is injective by A1;
  then F is one-to-one;
  then
A6: the ObjectMap of F is one-to-one;
  F is faithful by A5;
  then
A7: the MorphMap of F is "1-1";
  F is surjective by A1;
  then F is full;
  then
A8: 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";
A9: [G.o,G.o] in [:the carrier of A,the carrier of A:] by ZFMISC_1:87;
A10: [o,o] in [:the carrier of B,the carrier of B:] by ZFMISC_1:87;
  then
A11: [o,o] in dom the ObjectMap of G by FUNCT_2:def 1;
A12: (the ObjectMap of F*H).(o,o)
  = ((the ObjectMap of F)*the ObjectMap of H).[o,o] by Def36
    .= ((the ObjectMap of F)*(the ObjectMap of F)").[o,o] by A1,Def38
    .= (id rng the ObjectMap of F).[o,o] by A6,FUNCT_1:39
    .= (id dom(the ObjectMap of G)).[o,o] by A2,A6,FUNCT_1:33
    .= (id[:the carrier of B,the carrier of B:]).[o,o] by FUNCT_2:def 1
    .= [o,o] by A10,FUNCT_1:18;
A13: F.(G.o) = (F*H).o by Th33
    .= o by A12;
  dom the MorphMap of F = [:the carrier of A,the carrier of A:]
  by PARTFUN1:def 2;
  then [G.o,G.o] in dom the MorphMap of F by ZFMISC_1:87;
  then
A14: Morph-Map(F,G.o,G.o) is one-to-one by A7;
  [G.o,G.o] in dom the ObjectMap of F by A9,FUNCT_2:def 1;
  then ((the Arrows of B)*the ObjectMap of F).[G.o,G.o]
  = (the Arrows of B).((the ObjectMap of F).(G.o,G.o)) by FUNCT_1:13
    .= (the Arrows of B).(F.(G.o),F.(G.o)) by Def10;
  then
A15: ((the Arrows of B)*the ObjectMap of F).[G.o,G.o] <> {} by ALTCAT_2:def 6;
  Morph-Map(F,G.o,G.o) is Function of (the Arrows of A).[G.o,G.o],
  ((the Arrows of B)*the ObjectMap of F).[G.o,G.o] by A3,A9,PBOOLE:def 15;
  then
A16: dom Morph-Map(F,G.o,G.o)
  = (the Arrows of A).(G.o,G.o) by A15,FUNCT_2:def 1
    .= <^G.o,G.o^> by ALTCAT_1:def 1;
  ((the Arrows of A)*the ObjectMap of G).[o,o]
  = (the Arrows of A).((the ObjectMap of H).(o,o)) by A11,FUNCT_1:13
    .= (the Arrows of A).(G.o,G.o) by Def10;
  then
A17: ((the Arrows of A)*the ObjectMap of G).[o,o] <> {} by ALTCAT_2:def 6;
  the MorphMap of G is ManySortedFunction of
  the Arrows of B,(the Arrows of A)*the ObjectMap of G by Def4;
  then Morph-Map(G,o,o) is Function of (the Arrows of B).[o,o],
  ((the Arrows of A)*the ObjectMap of G).[o,o] by A10,PBOOLE:def 15;
  then
A18: dom Morph-Map(G,o,o) = (the Arrows of B).(o,o) by A17,FUNCT_2:def 1
    .= <^o,o^> by ALTCAT_1:def 1;
  then
A19: idm o in dom Morph-Map(G,o,o) by ALTCAT_1:19;
A20: Morph-Map(G,o,o)
  = f"".((the ObjectMap of G).(o,o)) by A2,A4,A11,FUNCT_1:13
    .= f"".[H.o,H.o] by Def10
    .= Morph-Map(F,G.o,G.o)" by A3,A7,A8,A9,MSUALG_3:def 4;
  Morph-Map(G,o,o).idm o in rng Morph-Map(G,o,o) by A19,FUNCT_1:def 3;
  then
A21: Morph-Map(G,o,o).idm o in dom Morph-Map(F,G.o,G.o) by A14,A20,FUNCT_1:33;
  Morph-Map(F,G.o,G.o).(Morph-Map(G,o,o).idm o)
  = (Morph-Map(F,G.o,G.o)*Morph-Map(G,o,o)).idm o by A18,ALTCAT_1:19,FUNCT_1:13
    .= (id rng Morph-Map(F,G.o,G.o)).idm o by A14,A20,FUNCT_1:39
    .= (id dom Morph-Map(G,o,o)).idm o by A14,A20,FUNCT_1:33
    .= idm F.(G.o) by A13,A18
    .= Morph-Map(F,G.o,G.o).idm G.o by Def20;
  hence thesis by A14,A16,A21;
end;

theorem Th38:
  for A,B being transitive with_units non empty AltCatStr,
  F being feasible FunctorStr over A,B st F is bijective Covariant
  holds F" is Covariant
proof
  let A,B be transitive with_units non empty AltCatStr,
  F be feasible FunctorStr over A,B;
  assume
A1: F is bijective Covariant;
  then F is injective;
  then F is one-to-one;
  then
A2: the ObjectMap of F is one-to-one;
  F is surjective by A1;
  then F is onto;
  then
A3: the ObjectMap of F is onto;
  the ObjectMap of F is Covariant by A1;
  then consider f being Function of the carrier of A, the carrier of B
  such that
A4: the ObjectMap of F = [:f,f:];
A5: f is one-to-one by A2,A4,Th7;
  then
A6: dom(f") = rng f by FUNCT_1:33;
A7: rng(f") = dom f by A5,FUNCT_1:33;
A8: rng[:f,f:] = [:the carrier of B,the carrier of B:] by A3,A4;
  rng[:f,f:] = [:rng f,rng f:] by FUNCT_3:67;
  then rng f = the carrier of B by A8,ZFMISC_1:92;
  then reconsider g = f" as Function of the carrier of B, the carrier of A
  by A6,A7,FUNCT_2:def 1,RELSET_1:4;
  take g;
  [:f,f:]" = [:g,g:] by A5,Th6;
  hence thesis by A1,A4,Def38;
end;

theorem Th39:
  for A,B being transitive with_units non empty AltCatStr,
  F being feasible FunctorStr over A,B st F is bijective Contravariant
  holds F" is Contravariant
proof
  let A,B be transitive with_units non empty AltCatStr,
  F be feasible FunctorStr over A,B;
  assume
A1: F is bijective Contravariant;
  then F is injective;
  then F is one-to-one;
  then
A2: the ObjectMap of F is one-to-one;
  F is surjective by A1;
  then F is onto;
  then
A3: the ObjectMap of F is onto;
  the ObjectMap of F is Contravariant by A1;
  then consider f being Function of the carrier of A, the carrier of B
  such that
A4: the ObjectMap of F = ~[:f,f:];
  [:f,f:] is one-to-one by A2,A4,Th9;
  then
A5: f is one-to-one by Th7;
  then
A6: dom(f") = rng f by FUNCT_1:33;
A7: rng(f") = dom f by A5,FUNCT_1:33;
  [:f,f:] is onto by A3,A4,Th13;
  then
A8: rng[:f,f:] = [:the carrier of B,the carrier of B:];
  rng[:f,f:] = [:rng f,rng f:] by FUNCT_3:67;
  then rng f = the carrier of B by A8,ZFMISC_1:92;
  then reconsider g = f" as Function of the carrier of B, the carrier of A
  by A6,A7,FUNCT_2:def 1,RELSET_1:4;
  take g;
A9: [:f,f:]" = [:g,g:] by A5,Th6;
  thus the ObjectMap of F" = (the ObjectMap of F)" by A1,Def38
    .= ~[:g,g:] by A4,A5,A9,Th10;
end;

theorem Th40:
  for A,B being transitive with_units non empty AltCatStr,
  F being feasible reflexive FunctorStr over A,B
  st F is bijective coreflexive Covariant
  for o1,o2 being Object of B, m being Morphism of o1,o2 st <^o1,o2^> <> {}
  holds Morph-Map(F,F".o1,F".o2).(Morph-Map(F",o1,o2).m) = m
proof
  let A,B be transitive with_units non empty AltCatStr,
  F be feasible reflexive FunctorStr over A,B such that
A1: F is bijective coreflexive Covariant;
  set G = F";
A2: G is Covariant by A1,Th38;
  reconsider H = G as feasible reflexive FunctorStr over B,A by A1,Th35,Th36;
A3: the ObjectMap of G = (the ObjectMap of F)" by A1,Def38;
  consider f being ManySortedFunction of (the Arrows of A),
  (the Arrows of B)*the ObjectMap of F such that
A4: f = the MorphMap of F and
A5: the MorphMap of G = f""*(the ObjectMap of F)" by A1,Def38;
  F is injective by A1;
  then F is faithful;
  then
A6: the MorphMap of F is "1-1";
  F is surjective by A1;
  then F is full;
  then
A7: 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";
  let o1,o2 be Object of B, m be Morphism of o1,o2 such that
A8: <^o1,o2^> <> {};
A9: [G.o1,G.o2] in [:the carrier of A,the carrier of A:] by ZFMISC_1:87;
A10: [o1,o2] in [:the carrier of B,the carrier of B:] by ZFMISC_1:87;
  then
A11: [o1,o2] in dom the ObjectMap of G by FUNCT_2:def 1;
  dom the MorphMap of F = [:the carrier of A,the carrier of A:]
  by PARTFUN1:def 2;
  then [G.o1,G.o2] in dom the MorphMap of F by ZFMISC_1:87;
  then
A12: Morph-Map(F,G.o1,G.o2) is one-to-one by A6;
  ((the Arrows of A)*the ObjectMap of G).[o1,o2]
  = (the Arrows of A).((the ObjectMap of H).(o1,o2)) by A11,FUNCT_1:13
    .= (the Arrows of A).(H.o1,H.o2) by A2,Th22
    .= <^H.o1,H.o2^> by ALTCAT_1:def 1;
  then
A13: ((the Arrows of A)*the ObjectMap of G).[o1,o2] <> {} by A2,A8,Def18;
  the MorphMap of G is ManySortedFunction of
  the Arrows of B,(the Arrows of A)*the ObjectMap of G by Def4;
  then Morph-Map(G,o1,o2) is Function of (the Arrows of B).[o1,o2],
  ((the Arrows of A)*the ObjectMap of G).[o1,o2] by A10,PBOOLE:def 15;
  then
A14: dom Morph-Map(G,o1,o2) = (the Arrows of B).(o1,o2) by A13,FUNCT_2:def 1
    .= <^o1,o2^> by ALTCAT_1:def 1;
A15: Morph-Map(G,o1,o2)
  = f"".((the ObjectMap of G).(o1,o2)) by A3,A5,A11,FUNCT_1:13
    .= f"".[H.o1,H.o2] by A2,Th22
    .= Morph-Map(F,G.o1,G.o2)" by A4,A6,A7,A9,MSUALG_3:def 4;
  thus Morph-Map(F,G.o1,G.o2).(Morph-Map(G,o1,o2).m)
  = (Morph-Map(F,G.o1,G.o2)*Morph-Map(G,o1,o2)).m by A8,A14,FUNCT_1:13
    .= (id rng Morph-Map(F,G.o1,G.o2)).m by A12,A15,FUNCT_1:39
    .= (id dom Morph-Map(G,o1,o2)).m by A12,A15,FUNCT_1:33
    .= m by A14;
end;

theorem Th41:
  for A,B being transitive with_units non empty AltCatStr,
  F being feasible reflexive FunctorStr over A,B
  st F is bijective coreflexive Contravariant
  for o1,o2 being Object of B, m being Morphism of o1,o2 st <^o1,o2^> <> {}
  holds Morph-Map(F,F".o2,F".o1).(Morph-Map(F",o1,o2).m) = m
proof
  let A,B be transitive with_units non empty AltCatStr,
  F be feasible reflexive FunctorStr over A,B such that
A1: F is bijective coreflexive Contravariant;
  set G = F";
A2: G is Contravariant by A1,Th39;
  reconsider H = G as feasible reflexive FunctorStr over B,A by A1,Th35,Th36;
A3: the ObjectMap of G = (the ObjectMap of F)" by A1,Def38;
  consider f being ManySortedFunction of (the Arrows of A),
  (the Arrows of B)*the ObjectMap of F such that
A4: f = the MorphMap of F and
A5: the MorphMap of G = f""*(the ObjectMap of F)" by A1,Def38;
  F is injective by A1;
  then F is faithful;
  then
A6: the MorphMap of F is "1-1";
  F is surjective by A1;
  then F is full;
  then
A7: 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";
  let o1,o2 be Object of B, m be Morphism of o1,o2 such that
A8: <^o1,o2^> <> {};
A9: [G.o2,G.o1] in [:the carrier of A,the carrier of A:] by ZFMISC_1:87;
A10: [o1,o2] in [:the carrier of B,the carrier of B:] by ZFMISC_1:87;
  then
A11: [o1,o2] in dom the ObjectMap of G by FUNCT_2:def 1;
  dom the MorphMap of F = [:the carrier of A,the carrier of A:]
  by PARTFUN1:def 2;
  then [G.o2,G.o1] in dom the MorphMap of F by ZFMISC_1:87;
  then
A12: Morph-Map(F,G.o2,G.o1) is one-to-one by A6;
  ((the Arrows of A)*the ObjectMap of G).[o1,o2]
  = (the Arrows of A).((the ObjectMap of H).(o1,o2)) by A11,FUNCT_1:13
    .= (the Arrows of A).(H.o2,H.o1) by A2,Th23
    .= <^H.o2,H.o1^> by ALTCAT_1:def 1;
  then
A13: ((the Arrows of A)*the ObjectMap of G).[o1,o2] <> {} by A2,A8,Def19;
  the MorphMap of G is ManySortedFunction of
  the Arrows of B,(the Arrows of A)*the ObjectMap of G by Def4;
  then Morph-Map(G,o1,o2) is Function of (the Arrows of B).[o1,o2],
  ((the Arrows of A)*the ObjectMap of G).[o1,o2] by A10,PBOOLE:def 15;
  then
A14: dom Morph-Map(G,o1,o2) = (the Arrows of B).(o1,o2) by A13,FUNCT_2:def 1
    .= <^o1,o2^> by ALTCAT_1:def 1;
A15: Morph-Map(G,o1,o2)
  = f"".((the ObjectMap of G).(o1,o2)) by A3,A5,A11,FUNCT_1:13
    .= f"".[H.o2,H.o1] by A2,Th23
    .= Morph-Map(F,G.o2,G.o1)" by A4,A6,A7,A9,MSUALG_3:def 4;
  thus Morph-Map(F,F".o2,F".o1).(Morph-Map(F",o1,o2).m)
  = (Morph-Map(F,G.o2,G.o1)*Morph-Map(G,o1,o2)).m by A8,A14,FUNCT_1:13
    .= (id rng Morph-Map(F,G.o2,G.o1)).m by A12,A15,FUNCT_1:39
    .= (id dom Morph-Map(G,o1,o2)).m by A12,A15,FUNCT_1:33
    .= m by A14;
end;

theorem Th42:
  for A,B being transitive with_units non empty AltCatStr,
  F being feasible reflexive FunctorStr over A,B st
  F is bijective comp-preserving Covariant coreflexive
  holds F" is comp-preserving
proof
  let A,B be transitive with_units non empty AltCatStr,
  F be feasible reflexive FunctorStr over A,B such that
A1: F is bijective comp-preserving Covariant coreflexive;
  set G = F";
A2: G is Covariant by A1,Th38;
  reconsider H = G as feasible reflexive FunctorStr over B,A by A1,Th35,Th36;
A3: the ObjectMap of G = (the ObjectMap of F)" by A1,Def38;
  consider ff being ManySortedFunction of (the Arrows of A),
  (the Arrows of B)*the ObjectMap of F such that
A4: ff = the MorphMap of F and
A5: the MorphMap of G = ff""*(the ObjectMap of F)" by A1,Def38;
A6: F is injective by A1;
  then F is one-to-one;
  then
A7: the ObjectMap of F is one-to-one;
  F is faithful by A6;
  then
A8: the MorphMap of F is "1-1";
  F is surjective by A1;
  then F is full;
  then
A9: 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";
  let o1,o2,o3 be Object of B;
  assume
A10: <^o1,o2^> <> {};
  then
A11: <^H.o1,H.o2^> <> {} by A2,Def18;
  assume
A12: <^o2,o3^> <> {};
  then
A13: <^H.o2,H.o3^> <> {} by A2,Def18;
A14: <^o1,o3^> <> {} by A10,A12,ALTCAT_1:def 2;
  then
A15: <^H.o1,H.o3^> <> {} by A2,Def18;
  then
A16: <^F.(G.o1),F.(G.o3)^> <> {} by A1,Def18;
  let f be Morphism of o1,o2, g be Morphism of o2,o3;
  reconsider K = G as Covariant FunctorStr over B,A by A1,Th38;
  K.f = Morph-Map(K,o1,o2).f by A10,A11,Def15;
  then reconsider f9 = Morph-Map(K,o1,o2).f as Morphism of G.o1,G.o2;
  K.g = Morph-Map(K,o2,o3).g by A12,A13,Def15;
  then reconsider g9 = Morph-Map(K,o2,o3).g as Morphism of G.o2,G.o3;
  take f9,g9;
  thus f9 = Morph-Map(G,o1,o2).f;
  thus g9 = Morph-Map(G,o2,o3).g;
  consider f99 being Morphism of F.(G.o1),F.(G.o2),
  g99 being Morphism of F.(G.o2),F.(G.o3) such that
A17: f99 = Morph-Map(F,G.o1,G.o2).f9 and
A18: g99 = Morph-Map(F,G.o2,G.o3).g9 and
A19: Morph-Map(F,G.o1,G.o3).(g9*f9) = g99*f99 by A1,A11,A13;
A20: g = g99 by A1,A12,A18,Th40;
A21: f = f99 by A1,A10,A17,Th40;
A22: [G.o1,G.o3] in [:the carrier of A,the carrier of A:] by ZFMISC_1:87;
A23: [o1,o3] in [:the carrier of B,the carrier of B:] by ZFMISC_1:87;
  then
A24: [o1,o3] in dom the ObjectMap of G by FUNCT_2:def 1;
  dom the MorphMap of F = [:the carrier of A,the carrier of A:]
  by PARTFUN1:def 2;
  then [G.o1,G.o3] in dom the MorphMap of F by ZFMISC_1:87;
  then
A25: Morph-Map(F,G.o1,G.o3) is one-to-one by A8;
  [G.o1,G.o3] in dom the ObjectMap of F by A22,FUNCT_2:def 1;
  then
A26: ((the Arrows of B)*the ObjectMap of F).[G.o1,G.o3]
  = (the Arrows of B).((the ObjectMap of F).(G.o1,G.o3)) by FUNCT_1:13
    .= (the Arrows of B).(F.(G.o1),F.(G.o3)) by A1,Th22
    .= <^F.(G.o1),F.(G.o3)^> by ALTCAT_1:def 1;
  Morph-Map(F,G.o1,G.o3) is Function of (the Arrows of A).[G.o1,G.o3],
  ((the Arrows of B)*the ObjectMap of F).[G.o1,G.o3] by A4,A22,PBOOLE:def 15;
  then
A27: dom Morph-Map(F,G.o1,G.o3)
  = (the Arrows of A).(G.o1,G.o3) by A16,A26,FUNCT_2:def 1
    .= <^G.o1,G.o3^> by ALTCAT_1:def 1;
A28: ((the Arrows of A)*the ObjectMap of G).[o1,o3]
  = (the Arrows of A).((the ObjectMap of H).(o1,o3)) by A24,FUNCT_1:13
    .= (the Arrows of A).(G.o1,G.o3) by A2,Th22
    .= <^G.o1,G.o3^> by ALTCAT_1:def 1;
  the MorphMap of G is ManySortedFunction of
  the Arrows of B,(the Arrows of A)*the ObjectMap of G by Def4;
  then Morph-Map(G,o1,o3) is Function of (the Arrows of B).[o1,o3],
  ((the Arrows of A)*the ObjectMap of G).[o1,o3] by A23,PBOOLE:def 15;
  then
A29: dom Morph-Map(G,o1,o3)
  = (the Arrows of B).(o1,o3) by A15,A28,FUNCT_2:def 1
    .= <^o1,o3^> by ALTCAT_1:def 1;
A30: Morph-Map(G,o1,o3)
  = ff"".((the ObjectMap of G).(o1,o3)) by A3,A5,A24,FUNCT_1:13
    .= ff"".[H.o1,H.o3] by A2,Th22
    .= Morph-Map(F,G.o1,G.o3)" by A4,A8,A9,A22,MSUALG_3:def 4;
A31: the ObjectMap of F*H = (the ObjectMap of F)*the ObjectMap of H by Def36
    .= (the ObjectMap of F)*(the ObjectMap of F)" by A1,Def38
    .= id rng the ObjectMap of F by A7,FUNCT_1:39
    .= id dom the ObjectMap of G by A3,A7,FUNCT_1:33
    .= id[:the carrier of B,the carrier of B:] by FUNCT_2:def 1;
  [o1,o1] in [:the carrier of B,the carrier of B:] by ZFMISC_1:87;
  then
A32: (the ObjectMap of F*H).(o1,o1) = [o1,o1] by A31,FUNCT_1:18;
A33: F.(G.o1) = (F*H).o1 by Th33
    .= o1 by A32;
  [o2,o2] in [:the carrier of B,the carrier of B:] by ZFMISC_1:87;
  then
A34: (the ObjectMap of F*H).(o2,o2) = [o2,o2] by A31,FUNCT_1:18;
A35: F.(G.o2) = (F*H).o2 by Th33
    .= o2 by A34;
  [o3,o3] in [:the carrier of B,the carrier of B:] by ZFMISC_1:87;
  then
A36: (the ObjectMap of F*H).(o3,o3) = [o3,o3] by A31,FUNCT_1:18;
A37: F.(G.o3) = (F*H).o3 by Th33
    .= o3 by A36;
  Morph-Map(G,o1,o3).(g*f) in rng Morph-Map(G,o1,o3) by A14,A29,FUNCT_1:def 3;
  then
A38: Morph-Map(G,o1,o3).(g*f) in dom Morph-Map(F,G.o1,G.o3) by A25,A30,
FUNCT_1:33;
  Morph-Map(F,G.o1,G.o3).(Morph-Map(G,o1,o3).(g*f))
  = Morph-Map(F,G.o1,G.o3).(g9*f9) by A1,A14,A19,A20,A21,A33,A35,A37,Th40;
  hence thesis by A25,A27,A38;
end;

theorem Th43:
  for A,B being transitive with_units non empty AltCatStr,
  F being feasible reflexive FunctorStr over A,B st
  F is bijective comp-reversing Contravariant coreflexive
  holds F" is comp-reversing
proof
  let A,B be transitive with_units non empty AltCatStr,
  F be feasible reflexive FunctorStr over A,B such that
A1: F is bijective comp-reversing Contravariant coreflexive;
  set G = F";
A2: G is Contravariant by A1,Th39;
  reconsider H = G as feasible reflexive FunctorStr over B,A by A1,Th35,Th36;
A3: the ObjectMap of G = (the ObjectMap of F)" by A1,Def38;
  consider ff being ManySortedFunction of (the Arrows of A),
  (the Arrows of B)*the ObjectMap of F such that
A4: ff = the MorphMap of F and
A5: the MorphMap of G = ff""*(the ObjectMap of F)" by A1,Def38;
A6: F is injective by A1;
  then F is one-to-one;
  then
A7: the ObjectMap of F is one-to-one;
  F is faithful by A6;
  then
A8: the MorphMap of F is "1-1";
  F is surjective by A1;
  then F is full;
  then
A9: 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";
  let o1,o2,o3 be Object of B;
  assume
A10: <^o1,o2^> <> {};
  then
A11: <^H.o2,H.o1^> <> {} by A2,Def19;
  assume
A12: <^o2,o3^> <> {};
  then
A13: <^H.o3,H.o2^> <> {} by A2,Def19;
A14: <^o1,o3^> <> {} by A10,A12,ALTCAT_1:def 2;
  then
A15: <^H.o3,H.o1^> <> {} by A2,Def19;
  then
A16: <^F.(G.o1),F.(G.o3)^> <> {} by A1,Def19;
  let f be Morphism of o1,o2, g be Morphism of o2,o3;
  reconsider K = G as Contravariant FunctorStr over B,A by A1,Th39;
  K.f = Morph-Map(K,o1,o2).f by A10,A11,Def16;
  then reconsider f9 = Morph-Map(K,o1,o2).f as Morphism of G.o2,G.o1;
  K.g = Morph-Map(K,o2,o3).g by A12,A13,Def16;
  then reconsider g9 = Morph-Map(K,o2,o3).g as Morphism of G.o3,G.o2;
  take f9,g9;
  thus f9 = Morph-Map(G,o1,o2).f;
  thus g9 = Morph-Map(G,o2,o3).g;
  consider g99 being Morphism of F.(G.o2),F.(G.o3),
  f99 being Morphism of F.(G.o1),F.(G.o2) such that
A17: g99 = Morph-Map(F,G.o3,G.o2).g9 and
A18: f99 = Morph-Map(F,G.o2,G.o1).f9 and
A19: Morph-Map(F,G.o3,G.o1).(f9*g9) = g99*f99 by A1,A11,A13;
A20: g = g99 by A1,A12,A17,Th41;
A21: f = f99 by A1,A10,A18,Th41;
A22: [G.o3,G.o1] in [:the carrier of A,the carrier of A:] by ZFMISC_1:87;
A23: [o1,o3] in [:the carrier of B,the carrier of B:] by ZFMISC_1:87;
  then
A24: [o1,o3] in dom the ObjectMap of G by FUNCT_2:def 1;
  dom the MorphMap of F = [:the carrier of A,the carrier of A:]
  by PARTFUN1:def 2;
  then [G.o3,G.o1] in dom the MorphMap of F by ZFMISC_1:87;
  then
A25: Morph-Map(F,G.o3,G.o1) is one-to-one by A8;
  [G.o3,G.o1] in dom the ObjectMap of F by A22,FUNCT_2:def 1;
  then
A26: ((the Arrows of B)*the ObjectMap of F).[G.o3,G.o1]
  = (the Arrows of B).((the ObjectMap of F).(G.o3,G.o1)) by FUNCT_1:13
    .= (the Arrows of B).(F.(G.o1),F.(G.o3)) by A1,Th23
    .= <^F.(G.o1),F.(G.o3)^> by ALTCAT_1:def 1;
  Morph-Map(F,G.o3,G.o1) is Function of (the Arrows of A).[G.o3,G.o1],
  ((the Arrows of B)*the ObjectMap of F).[G.o3,G.o1] by A4,A22,PBOOLE:def 15;
  then
A27: dom Morph-Map(F,G.o3,G.o1)
  = (the Arrows of A).(G.o3,G.o1) by A16,A26,FUNCT_2:def 1
    .= <^G.o3,G.o1^> by ALTCAT_1:def 1;
A28: ((the Arrows of A)*the ObjectMap of G).[o1,o3]
  = (the Arrows of A).((the ObjectMap of H).(o1,o3)) by A24,FUNCT_1:13
    .= (the Arrows of A).(G.o3,G.o1) by A2,Th23
    .= <^G.o3,G.o1^> by ALTCAT_1:def 1;
  the MorphMap of G is ManySortedFunction of
  the Arrows of B,(the Arrows of A)*the ObjectMap of G by Def4;
  then Morph-Map(G,o1,o3) is Function of (the Arrows of B).[o1,o3],
  ((the Arrows of A)*the ObjectMap of G).[o1,o3] by A23,PBOOLE:def 15;
  then
A29: dom Morph-Map(G,o1,o3)
  = (the Arrows of B).(o1,o3) by A15,A28,FUNCT_2:def 1
    .= <^o1,o3^> by ALTCAT_1:def 1;
A30: Morph-Map(G,o1,o3)
  = ff"".((the ObjectMap of G).(o1,o3)) by A3,A5,A24,FUNCT_1:13
    .= ff"".[H.o3,H.o1] by A2,Th23
    .= Morph-Map(F,G.o3,G.o1)" by A4,A8,A9,A22,MSUALG_3:def 4;
A31: the ObjectMap of F*H = (the ObjectMap of F)*the ObjectMap of H by Def36
    .= (the ObjectMap of F)*(the ObjectMap of F)" by A1,Def38
    .= id rng the ObjectMap of F by A7,FUNCT_1:39
    .= id dom the ObjectMap of G by A3,A7,FUNCT_1:33
    .= id[:the carrier of B,the carrier of B:] by FUNCT_2:def 1;
  [o1,o1] in [:the carrier of B,the carrier of B:] by ZFMISC_1:87;
  then
A32: (the ObjectMap of F*H).(o1,o1) = [o1,o1] by A31,FUNCT_1:18;
A33: F.(G.o1) = (F*H).o1 by Th33
    .= o1 by A32;
  [o2,o2] in [:the carrier of B,the carrier of B:] by ZFMISC_1:87;
  then
A34: (the ObjectMap of F*H).(o2,o2) = [o2,o2] by A31,FUNCT_1:18;
A35: F.(G.o2) = (F*H).o2 by Th33
    .= o2 by A34;
  [o3,o3] in [:the carrier of B,the carrier of B:] by ZFMISC_1:87;
  then
A36: (the ObjectMap of F*H).(o3,o3) = [o3,o3] by A31,FUNCT_1:18;
A37: F.(G.o3) = (F*H).o3 by Th33
    .= o3 by A36;
  Morph-Map(G,o1,o3).(g*f) in rng Morph-Map(G,o1,o3) by A14,A29,FUNCT_1:def 3;
  then
A38: Morph-Map(G,o1,o3).(g*f) in dom Morph-Map(F,G.o3,G.o1) by A25,A30,
FUNCT_1:33;
  Morph-Map(F,G.o3,G.o1).(Morph-Map(G,o1,o3).(g*f))
  = Morph-Map(F,G.o3,G.o1).(f9*g9) by A1,A14,A19,A20,A21,A33,A35,A37,Th41;
  hence thesis by A25,A27,A38;
end;

registration
  let C1 be 1-sorted, C2 be non empty 1-sorted;
  cluster Covariant -> reflexive for BimapStr over C1,C2;
  coherence
  proof
    let M be BimapStr over C1,C2;
    assume M is Covariant;
    then the ObjectMap of M is Covariant;
    then ex f being Function of the carrier of C1, the carrier of C2
    st the ObjectMap of M = [:f,f:];
    hence
    (the ObjectMap of M).:id the carrier of C1 c= id the carrier of C2 by Th14;
  end;
end;

registration
  let C1 be 1-sorted, C2 be non empty 1-sorted;
  cluster Contravariant -> reflexive for BimapStr over C1,C2;
  coherence
  proof
    let M be BimapStr over C1,C2;
    assume M is Contravariant;
    then the ObjectMap of M is Contravariant;
    then consider f being Function of the carrier of C1, the carrier of C2
    such that
A1: the ObjectMap of M = ~[:f,f:];
    (~[:f,f:]).:id the carrier of C1 = [:f,f:].:id the carrier of C1 by Th3;
    hence
    (the ObjectMap of M).:id the carrier of C1 c= id the carrier of C2
    by A1,Th14;
  end;
end;

theorem Th44:
  for C1,C2 being 1-sorted, M being BimapStr over C1,C2
  st M is Covariant onto holds M is coreflexive
proof
  let C1,C2 be 1-sorted;
  let M be BimapStr over C1,C2;
  assume
A1: M is Covariant onto;
  then the ObjectMap of M is Covariant;
  then consider f being Function of the carrier of C1, the carrier of C2
  such that
A2: the ObjectMap of M = [:f,f:];
  the ObjectMap of M is onto by A1;
  then f is onto by A2,Th4;
  hence
  id the carrier of C2 c= (the ObjectMap of M).:id the carrier of C1
  by A2,Th11;
end;

theorem Th45:
  for C1,C2 being 1-sorted, M being BimapStr over C1,C2
  st M is Contravariant onto holds M is coreflexive
proof
  let C1,C2 be 1-sorted;
  let M be BimapStr over C1,C2;
  assume
A1: M is Contravariant onto;
  then the ObjectMap of M is Contravariant;
  then consider f being Function of the carrier of C1, the carrier of C2
  such that
A2: the ObjectMap of M = ~[:f,f:];
  the ObjectMap of M is onto by A1;
  then [:f,f:] is onto by A2,Th13;
  then
A3: f is onto by Th4;
  (the ObjectMap of M).:id the carrier of C1
  = [:f,f:].:id the carrier of C1 by A2,Th3;
  hence
  id the carrier of C2 c= (the ObjectMap of M).:id the carrier of C1
  by A3,Th11;
end;

registration
  let C1 be transitive with_units non empty AltCatStr,
  C2 be with_units non empty AltCatStr;
  cluster covariant -> reflexive for Functor of C1,C2;
  coherence;
end;

registration
  let C1 be transitive with_units non empty AltCatStr,
  C2 be with_units non empty AltCatStr;
  cluster contravariant -> reflexive for Functor of C1,C2;
  coherence;
end;

theorem Th46:
  for C1 being transitive with_units non empty AltCatStr,
  C2 being with_units non empty AltCatStr,
  F being Functor of C1,C2 st F is covariant onto holds F is coreflexive
by Th44;

theorem Th47:
  for C1 being transitive with_units non empty AltCatStr,
  C2 being with_units non empty AltCatStr,
  F being Functor of C1,C2 st F is contravariant onto holds F is coreflexive
by Th45;

theorem Th48:
  for A,B being transitive with_units non empty AltCatStr,
  F being covariant Functor of A,B st F is bijective
  ex G being Functor of B,A st G = F" & G is bijective covariant
proof
  let A,B be transitive with_units non empty AltCatStr,
  F be covariant Functor of A,B;
  assume
A1: F is bijective;
  then F is injective;
  then F is one-to-one;
  then
A2: the ObjectMap of F is one-to-one;
A3: F is feasible by Def25;
  then
A4: F" is bijective feasible by A1,Th35;
A5: F is id-preserving by Def25;
A6: F is comp-preserving by Def26;
  F is surjective by A1;
  then
A7: F is onto;
  then
A8: the ObjectMap of F is onto;
A9: F is Covariant by Def26;
A10: F is coreflexive by A7,Th46;
A11: F" is Covariant proof F is Covariant by Def26;
    then the ObjectMap of F is Covariant;
    then consider f being Function of the carrier of A, the carrier of B
    such that
A12: the ObjectMap of F = [:f,f:];
A13: f is one-to-one by A2,A12,Th7;
    then
A14: dom(f") = rng f by FUNCT_1:33;
A15: rng(f") = dom f by A13,FUNCT_1:33;
A16: rng[:f,f:] = [:the carrier of B,the carrier of B:]
    by A8,A12;
    rng[:f,f:] = [:rng f,rng f:] by FUNCT_3:67;
    then rng f = the carrier of B by A16,ZFMISC_1:92;
    then reconsider g = f" as Function of the carrier of B, the carrier of A
    by A14,A15,FUNCT_2:def 1,RELSET_1:4;
    take g;
    [:f,f:]" = [:g,g:] by A13,Th6;
    hence thesis by A1,A12,Def38;
  end;
A17: F" is id-preserving by A1,A3,A5,A10,Th37;
  F" is comp-preserving by A1,A3,A6,A9,A10,Th42;
  then reconsider G = F" as Functor of B,A by A4,A11,A17,Def25;
  take G;
  thus G = F";
  thus G is bijective by A1,A3,Th35;
  thus G is Covariant by A11;
  thus thesis by A1,A3,A6,A9,A10,Th42;
end;

theorem Th49:
  for A,B being transitive with_units non empty AltCatStr,
  F being contravariant Functor of A,B st F is bijective
  ex G being Functor of B,A st G = F" & G is bijective contravariant
proof
  let A,B be transitive with_units non empty AltCatStr,
  F be contravariant Functor of A,B;
  assume
A1: F is bijective;
  then F is injective;
  then F is one-to-one;
  then
A2: the ObjectMap of F is one-to-one;
A3: F is feasible by Def25;
  then
A4: F" is bijective feasible by A1,Th35;
A5: F is id-preserving by Def25;
A6: F is comp-reversing by Def27;
  F is surjective by A1;
  then
A7: F is onto;
  then
A8: the ObjectMap of F is onto;
A9: F is Contravariant by Def27;
A10: F is coreflexive by A7,Th47;
A11: F" is Contravariant proof F is Contravariant by Def27;
    then the ObjectMap of F is Contravariant;
    then consider f being Function of the carrier of A, the carrier of B
    such that
A12: the ObjectMap of F = ~[:f,f:];
    [:f,f:] is one-to-one by A2,A12,Th9;
    then
A13: f is one-to-one by Th7;
    then
A14: dom(f") = rng f by FUNCT_1:33;
A15: rng(f") = dom f by A13,FUNCT_1:33;
    [:f,f:] is onto by A8,A12,Th13;
    then
A16: rng[:f,f:] = [:the carrier of B,the carrier of B:];
    rng[:f,f:] = [:rng f,rng f:] by FUNCT_3:67;
    then rng f = the carrier of B by A16,ZFMISC_1:92;
    then reconsider g = f" as Function of the carrier of B, the carrier of A
    by A14,A15,FUNCT_2:def 1,RELSET_1:4;
    take g;
A17: [:f,f:]" = [:g,g:] by A13,Th6;
    thus the ObjectMap of F" = (the ObjectMap of F)" by A1,Def38
      .= ~[:g,g:] by A12,A13,A17,Th10;
  end;
A18: F" is id-preserving by A1,A3,A5,A10,Th37;
  F" is comp-reversing by A1,A3,A6,A9,A10,Th43;
  then reconsider G = F" as Functor of B,A by A4,A11,A18,Def25;
  take G;
  thus G = F";
  thus G is bijective by A1,A3,Th35;
  thus G is Contravariant by A11;
  thus thesis by A1,A3,A6,A9,A10,Th43;
end;

definition
  let A,B be transitive with_units non empty AltCatStr;
  pred A,B are_isomorphic means
  ex F being Functor of A,B st F is bijective covariant;
  reflexivity
  proof
    let A be transitive with_units non empty AltCatStr;
    take id A;
    thus thesis;
  end;
  symmetry
  proof
    let A,B be transitive with_units non empty AltCatStr;
    given F being Functor of A,B such that
A1: F is bijective covariant;
    consider G being Functor of B,A such that G = F" and
A2: G is bijective covariant by A1,Th48;
    take G;
    thus thesis by A2;
  end;
  pred A,B are_anti-isomorphic means
  ex F being Functor of A,B st F is bijective contravariant;
  symmetry
  proof
    let A,B be transitive with_units non empty AltCatStr;
    given F being Functor of A,B such that
A3: F is bijective contravariant;
    consider G being Functor of B,A such that G = F" and
A4: G is bijective contravariant by A3,Th49;
    take G;
    thus thesis by A4;
  end;
end;