:: Category of Functors between Alternative Categories
::  by Robert Nieszczerzewski
::
:: Received June 12, 1997
:: Copyright (c) 1997-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 RELAT_2, ALTCAT_1, XBOOLE_0, MSUALG_6, FUNCTOR0, CAT_1, FUNCT_1,
      PZFMISC1, NATTRA_1, PBOOLE, STRUCT_0, SUBSET_1, REALSET1, RELAT_1,
      FUNCT_2, CARD_3, CAT_2, ZFMISC_1, TARSKI, FUNCTOR2;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCTOR0, XTUPLE_0, MCART_1,
      DOMAIN_1, RELAT_1, STRUCT_0, CARD_3, FUNCT_1, PBOOLE, FUNCT_2, BINOP_1,
      MULTOP_1, ALTCAT_1;
 constructors DOMAIN_1, CARD_3, FUNCTOR0, RELSET_1, XTUPLE_0;
 registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, ALTCAT_1, FUNCTOR0,
      PBOOLE, FUNCT_1, RELAT_1;
 requirements SUBSET, BOOLE;
 definitions ALTCAT_1;
 equalities ALTCAT_1, BINOP_1, XTUPLE_0;
 theorems MULTOP_1, FUNCT_2, ZFMISC_1, ALTCAT_1, PBOOLE, BINOP_1, TARSKI,
      ALTCAT_2, FUNCTOR0, CARD_3, XBOOLE_0, PARTFUN1, RELAT_1, XTUPLE_0;
 schemes TARSKI, PBOOLE, MSSUBFAM, XBOOLE_0;

begin

registration
  let A be transitive with_units non empty AltCatStr, B be with_units non
  empty AltCatStr;
  cluster -> feasible id-preserving for Functor of A, B;
  coherence by FUNCTOR0:def 25;
end;

registration
  let A be transitive with_units non empty AltCatStr, B be with_units non
  empty AltCatStr;
  cluster covariant -> Covariant comp-preserving for Functor of A, B;
  coherence by FUNCTOR0:def 26;
  cluster Covariant comp-preserving -> covariant for Functor of A, B;
  coherence by FUNCTOR0:def 26;
  cluster contravariant -> Contravariant comp-reversing for Functor of A, B;
  coherence by FUNCTOR0:def 27;
  cluster Contravariant comp-reversing -> contravariant for Functor of A, B;
  coherence by FUNCTOR0:def 27;
end;

theorem Th1:
  for A,B being transitive with_units non empty AltCatStr, F
being covariant Functor of A,B for a being Object of A holds F.idm a = idm (F.a
  )
proof
  let A,B be transitive with_units non empty AltCatStr, F be covariant
  Functor of A,B;
  let a be Object of A;
  <^a,a^> <> {} & <^F.a,F.a^> <> {} by ALTCAT_2:def 7;
  hence F.idm a = Morph-Map(F,a,a).idm a by FUNCTOR0:def 15
    .= idm (F.a) by FUNCTOR0:def 20;
end;

begin :: Transformations

definition
  let A,B be transitive with_units non empty AltCatStr,
      F1,F2 be Functor of A,B;
  pred F1 is_transformable_to F2 means

  for a being Object of A holds <^ F1.a,F2.a^> <> {};
  reflexivity by ALTCAT_2:def 7;
end;

theorem Th2:
  for A,B being transitive with_units non empty AltCatStr, F,F1,
  F2 being Functor of A,B holds F is_transformable_to F1 & F1
  is_transformable_to F2 implies F is_transformable_to F2
proof
  let A,B be transitive with_units non empty AltCatStr,
  F,F1,F2 be Functor of A,B;
  assume
A1: F is_transformable_to F1 & F1 is_transformable_to F2;
  let a be Object of A;
  <^F.a,F1.a^> <> {} & <^F1.a,F2.a^> <> {} by A1;
  hence thesis by ALTCAT_1:def 2;
end;

definition
  let A,B be transitive with_units non empty AltCatStr,
  F1,F2 be Functor of A,B;
  assume
A1: F1 is_transformable_to F2;
  mode transformation of F1,F2 -> ManySortedSet of the carrier of A means
    :Def2: for a being Object of A holds it.a is Morphism of F1.a,F2.a;
  existence
  proof
    defpred P[Object of A,object] means $2 in <^F1.$1,F2.$1^>;
A2: for a being Element of A ex j being object st P[a,j]
    proof
      let a be Element of A;
      <^F1.a,F2.a^> <> {} by A1;
      then ex j being object st j in <^F1.a,F2.a^> by XBOOLE_0:def 1;
      hence thesis;
    end;
    consider t being ManySortedSet of the carrier of A such that
A3: for a being Element of A holds P[a,t.a] from PBOOLE:sch 6(A2);
    take t;
    thus thesis by A3;
  end;
end;

definition
  let A,B be transitive with_units non empty AltCatStr;
  let F be Functor of A,B;
  func idt F -> transformation of F,F means
  :Def3:
  for a being Object of A holds it.a = idm (F.a);
  existence
  proof
    defpred P[Object of A,object] means $2 = idm (F.$1);
A1: for a being Element of A ex j being object st P[a,j];
    consider t being ManySortedSet of the carrier of A such that
A2: for a being Element of A holds P[a,t.a] from PBOOLE:sch 6(A1);
    for a be Object of A holds t.a is Morphism of F.a,F.a
    proof
      let a be Element of A;
      P[a,t.a] by A2;
      hence thesis;
    end;
    then t is transformation of F,F by Def2;
    hence thesis by A2;
  end;
  uniqueness
  proof
    let it1,it2 be transformation of F,F such that
A3: for a being Object of A holds it1.a = idm (F.a) and
A4: for a being Object of A holds it2.a = idm (F.a);
    now
      let a be object;
      assume a in the carrier of A;
      then reconsider o = a as Object of A;
      thus it1.a = idm (F.o) by A3
        .= it2.a by A4;
    end;
    hence it1 = it2 by PBOOLE:3;
  end;
end;

definition
  let A,B be transitive with_units non empty AltCatStr,
  F1,F2 be Functor of A,B;
  assume
A1: F1 is_transformable_to F2;
  let t be transformation of F1,F2;
  let a be Object of A;
  func t!a -> Morphism of F1.a, F2.a means
  :Def4:
  it = t.a;
  existence
  proof
    t.a is Morphism of F1.a,F2.a by A1,Def2;
    hence thesis;
  end;
  correctness;
end;

definition
  let A,B be transitive with_units non empty AltCatStr,
      F,F1,F2 be Functor of A,B;
  assume
A1: F is_transformable_to F1 & F1 is_transformable_to F2;
  let t1 be transformation of F,F1;
  let t2 be transformation of F1,F2;
  func t2`*`t1 -> transformation of F,F2 means
  :Def5:
  for a being Object of A holds it!a = (t2!a) * (t1!a);
  existence
  proof
    defpred P[Object of A,object] means $2 = (t2!$1) * (t1!$1);
A2: for a being Element of A ex j being object st P[a,j];
    consider t being ManySortedSet of the carrier of A such that
A3: for a being Element of A holds P[a,t.a] from PBOOLE:sch 6(A2);
A4: F is_transformable_to F2 by A1,Th2;
    for a be Object of A holds t.a is Morphism of F.a,F2.a
    proof
      let o be Element of A;
      P[o,t.o] by A3;
      hence thesis;
    end;
    then reconsider t9 = t as transformation of F,F2 by A4,Def2;
    take t9;
    let a be Element of A;
    P[a,t.a] by A3;
    hence thesis by A4,Def4;
  end;
  uniqueness
  proof
    let it1,it2 be transformation of F,F2 such that
A5: for a being Object of A holds it1!a = (t2!a)*(t1!a) and
A6: for a being Object of A holds it2!a = (t2!a)*(t1!a);
A7: F is_transformable_to F2 by A1,Th2;
    now
      let a be object;
      assume a in the carrier of A;
      then reconsider o = a as Object of A;
      thus (it1 qua ManySortedSet of the carrier of A).a = it1!o by A7,Def4
        .= (t2!o)*(t1!o) by A5
        .= it2!o by A6
        .= (it2 qua ManySortedSet of the carrier of A).a by A7,Def4;
    end;
    hence it1 = it2 by PBOOLE:3;
  end;
end;

theorem Th3:
  for A,B being transitive with_units non empty AltCatStr, F1,F2
being Functor of A,B holds F1 is_transformable_to F2 implies for t1,
  t2 being transformation of F1,F2 st for a being Object of A holds t1!a = t2!a
  holds t1 = t2
proof
  let A,B be transitive with_units non empty AltCatStr, F1,F2 be
  Functor of A,B;
  assume
A1: F1 is_transformable_to F2;
  let t1,t2 be transformation of F1,F2;
  assume
A2: for a being Object of A holds t1!a = t2!a;
  now
    let a be object;
    assume a in the carrier of A;
    then reconsider o = a as Object of A;
    thus (t1 qua ManySortedSet of the carrier of A).a = t1!o by A1,Def4
      .= t2!o by A2
      .= (t2 qua ManySortedSet of the carrier of A).a by A1,Def4;
  end;
  hence thesis by PBOOLE:3;
end;

theorem Th4:
  for A,B being transitive with_units non empty AltCatStr, F
being Functor of A,B holds for a being Object of A holds (idt F)!a =
  idm(F.a)
proof
  let A,B be transitive with_units non empty AltCatStr, F be
  Functor of A,B;
  let a be Object of A;
  thus (idt F)!a = (idt F qua ManySortedSet of the carrier of A).a by Def4
    .= idm (F.a) by Def3;
end;

theorem Th5:
  for A,B being transitive with_units non empty AltCatStr, F1,F2
  being Functor of A,B holds F1 is_transformable_to F2 implies for t
  being transformation of F1,F2 holds (idt F2)`*`t = t & t`*`(idt F1) = t
proof
  let A,B be transitive with_units non empty AltCatStr, F1,F2 be
  Functor of A,B;
  assume
A1: F1 is_transformable_to F2;
  let t be transformation of F1,F2;
  now
    let a be Object of A;
A2: <^F1.a,F2.a^> <> {} by A1;
    thus ((idt F2)`*`t)!a = ((idt F2)!a)*(t!a) by A1,Def5
      .= (idm(F2.a))*(t!a) by Th4
      .= t!a by A2,ALTCAT_1:20;
  end;
  hence (idt F2)`*`t = t by A1,Th3;
  now
    let a be Object of A;
A3: <^F1.a,F2.a^> <> {} by A1;
    thus (t`*`(idt F1))!a = (t!a)*((idt F1)!a) by A1,Def5
      .= (t!a)*(idm(F1.a)) by Th4
      .= t!a by A3,ALTCAT_1:def 17;
  end;
  hence thesis by A1,Th3;
end;

theorem Th6:
  for A,B being category, F,F1,F2,F3 being Functor of A,B
  holds F is_transformable_to F1 & F1 is_transformable_to F2 & F2
  is_transformable_to F3 implies for t1 being transformation of F,F1, t2 being
transformation of F1,F2, t3 being transformation of F2,F3 holds t3`*`t2`*`t1 =
  t3`*`(t2`*`t1)
proof
  let A,B be category, F,F1,F2,F3 be Functor of A,B;
  assume that
A1: F is_transformable_to F1 and
A2: F1 is_transformable_to F2 and
A3: F2 is_transformable_to F3;
  let t1 be transformation of F,F1, t2 be transformation of F1,F2, t3 be
  transformation of F2,F3;
A4: F1 is_transformable_to F3 by A2,A3,Th2;
A5: F is_transformable_to F2 by A1,A2,Th2;
  now
    let a be Object of A;
A6: <^F2.a,F3.a^> <> {} by A3;
A7: <^F.a,F1.a^> <> {} & <^F1.a,F2.a^> <> {} by A1,A2;
    thus (t3`*`t2`*`t1)!a = ((t3`*`t2)!a)*(t1!a) by A1,A4,Def5
      .= (t3!a)*(t2!a)*(t1!a) by A2,A3,Def5
      .= (t3!a)*((t2!a)*(t1!a)) by A7,A6,ALTCAT_1:21
      .= (t3!a)*((t2`*`t1)!a) by A1,A2,Def5
      .= (t3`*`(t2`*`t1))!a by A3,A5,Def5;
  end;
  hence thesis by A1,A4,Th2,Th3;
end;

begin :: Natural transformations

Lm1: for A,B being transitive with_units non empty AltCatStr, F,G being
covariant Functor of A,B for a,b being Object of A st <^a,b^> <> {} for f being
Morphism of a,b holds (idt F)!b*F.f = F.f*((idt F)!a)
proof
  let A,B be transitive with_units non empty AltCatStr, F,G be covariant
  Functor of A,B;
  let a,b be Object of A such that
A1: <^a,b^> <> {};
  let f be Morphism of a,b;
A2: <^a,a^> <> {} by ALTCAT_2:def 7;
A3: <^b,b^> <> {} by ALTCAT_2:def 7;
  thus (idt F)!b*F.f = idm(F.b)*F.f by Th4
    .= F.idm b*F.f by Th1
    .= F.(idm b*f) by A1,A3,FUNCTOR0:def 23
    .= F.f by A1,ALTCAT_1:20
    .= F.(f*idm a) by A1,ALTCAT_1:def 17
    .= F.f*F.idm a by A1,A2,FUNCTOR0:def 23
    .= F.f*idm(F.a) by Th1
    .= F.f*((idt F)!a) by Th4;
end;

definition
  let A,B be transitive with_units non empty AltCatStr, F1,F2 be covariant
  Functor of A,B;
  pred F1 is_naturally_transformable_to F2 means

  F1 is_transformable_to
F2 & ex t being transformation of F1,F2 st for a,b being Object of A st <^a,b^>
  <> {} for f being Morphism of a,b holds t!b*F1.f = F2.f*(t!a);
  reflexivity
proof
  let F be covariant Functor of A,B;
  thus F is_transformable_to F;
  take idt F;
  thus thesis by Lm1;
end;
end;

theorem
  for A,B be transitive with_units non empty AltCatStr, F be
  covariant Functor of A,B holds F is_naturally_transformable_to F;

Lm2: for A,B be category, F,F1,F2 be covariant Functor of A,B holds F
is_transformable_to F1 & F1 is_transformable_to F2 implies for t1 being
transformation of F,F1 st for a,b being Object of A st <^a,b^> <> {} for f
being Morphism of a,b holds t1!b*F.f = F1.f*(t1!a) for t2 being transformation
of F1,F2 st for a,b being Object of A st <^a,b^> <> {} for f being Morphism of
a,b holds t2!b*F1.f = F2.f*(t2!a) for a,b being Object of A st <^a,b^><>{} for
f being Morphism of a,b holds (t2`*`t1)!b*F.f = F2.f*((t2`*`t1)!a)
proof
  let A,B be category, F,F1,F2 be covariant Functor of A,B;
  assume that
A1: F is_transformable_to F1 and
A2: F1 is_transformable_to F2;
  let t1 be transformation of F,F1 such that
A3: for a,b being Object of A st <^a,b^> <> {} for f being Morphism of a
  ,b holds t1!b*F.f = F1.f*(t1!a);
  let t2 be transformation of F1,F2 such that
A4: for a,b being Object of A st <^a,b^> <> {} for f being Morphism of a
  ,b holds t2!b*F1.f = F2.f*(t2!a);
  let a,b be Object of A;
A5: <^F.b,F1.b^> <> {} by A1;
A6: <^F.a,F1.a^> <> {} by A1;
A7: <^F1.b,F2.b^> <> {} by A2;
A8: <^F1.a,F2.a^> <> {} by A2;
  assume
A9: <^a,b^> <> {};
  then
A10: <^F.a,F.b^> <> {} by FUNCTOR0:def 18;
  let f be Morphism of a,b;
A11: <^F2.a,F2.b^> <> {} by A9,FUNCTOR0:def 18;
A12: <^F1.a,F1.b^> <> {} by A9,FUNCTOR0:def 18;
  thus ((t2`*`t1)!b)*(F.f) = ((t2!b)*(t1!b))*F.f by A1,A2,Def5
    .= t2!b*(t1!b*F.f) by A10,A5,A7,ALTCAT_1:21
    .= t2!b*(F1.f*(t1!a)) by A3,A9
    .= t2!b*F1.f*(t1!a) by A6,A7,A12,ALTCAT_1:21
    .= F2.f*(t2!a)*(t1!a) by A4,A9
    .= F2.f*((t2!a)*(t1!a)) by A6,A8,A11,ALTCAT_1:21
    .= F2.f*((t2`*`t1)!a) by A1,A2,Def5;
end;

theorem Th8:
  for A,B be category, F,F1,F2 be covariant Functor of A,B holds F
is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 implies
  F is_naturally_transformable_to F2
proof
  let A,B be category, F,F1,F2 be covariant Functor of A,B;
  assume
A1: F is_transformable_to F1;
  given t1 being transformation of F,F1 such that
A2: for a,b being Object of A st <^a,b^> <> {} for f being Morphism of a
  ,b holds t1!b*F.f = F1.f*(t1!a);
  assume
A3: F1 is_transformable_to F2;
  given t2 being transformation of F1,F2 such that
A4: for a,b being Object of A st <^a,b^> <> {} for f being Morphism of a
  ,b holds t2!b*F1.f = F2.f*(t2!a);
  thus F is_transformable_to F2 by A1,A3,Th2;
  take t2`*`t1;
  thus thesis by A1,A2,A3,A4,Lm2;
end;

definition
  let A,B be transitive with_units non empty AltCatStr, F1,F2 be covariant
  Functor of A,B;
  assume
A1: F1 is_naturally_transformable_to F2;
  mode natural_transformation of F1,F2 -> transformation of F1,F2 means
    :Def7:
for a,b being Object of A st <^a,b^> <> {} for f being Morphism of a,b holds it
    !b*F1.f = F2.f*(it!a);
  existence by A1;
end;

definition
  let A,B be transitive with_units non empty AltCatStr, F be covariant
  Functor of A,B;
  redefine func idt F -> natural_transformation of F,F;
  coherence
  proof
    F is_naturally_transformable_to F & for a,b being Object of A st <^a,b
^> <> {} for f being Morphism of a,b holds (idt F)!b*F.f = F.f*((idt F)!a) by
Lm1;
    hence thesis by Def7;
  end;
end;

definition
  let A,B be category, F,F1,F2 be covariant Functor of A,B such that
A1: F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2;
  let t1 be natural_transformation of F,F1;
  let t2 be natural_transformation of F1,F2;
  func t2`*`t1 -> natural_transformation of F,F2 means
  :Def8:
  it = t2`*`t1;
  existence
  proof
A2: F is_naturally_transformable_to F2 by A1,Th8;
A3: ( for a,b being Object of A st <^a,b^> <> {} for f being Morphism of a
,b holds t1!b*F.f = F1.f*(t1!a))& for a,b being Object of A st <^a,b^> <> {}
    for f being Morphism of a,b holds t2!b*F1.f = F2.f*(t2!a) by A1,Def7;
    F is_transformable_to F1 & F1 is_transformable_to F2 by A1;
    then
    for a,b being Object of A st <^a,b^> <> {} for f being Morphism of a,b
    holds (t2`*`t1)!b*F.f = F2.f*((t2`*`t1)!a) by A3,Lm2;
    then t2`*`t1 is natural_transformation of F,F2 by A2,Def7;
    hence thesis;
  end;
  correctness;
end;

theorem
  for A,B be transitive with_units non empty AltCatStr, F1,F2 be
covariant Functor of A,B holds F1 is_naturally_transformable_to F2 implies for
t being natural_transformation of F1,F2 holds (idt F2)`*`t = t & t`*`(idt F1) =
  t
by Th5;

theorem
  for A,B be transitive with_units non empty AltCatStr, F,F1,F2 be
  covariant Functor of A,B holds F is_naturally_transformable_to F1 & F1
is_naturally_transformable_to F2 implies for t1 being natural_transformation of
F,F1 for t2 being natural_transformation of F1,F2 for a being Object of A holds
  (t2`*`t1)!a = (t2!a)*(t1!a)
by Def5;

theorem
  for A,B be category, F,F1,F2,F3 be covariant Functor of A,B for t be
  natural_transformation of F,F1, t1 be natural_transformation of F1,F2 holds F
  is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 & F2
is_naturally_transformable_to F3 implies for t3 being natural_transformation of
  F2,F3 holds t3`*`t1`*`t = t3`*`(t1`*`t)
proof
  let A,B be category, F,F1,F2,F3 be covariant Functor of A,B;
  let t be natural_transformation of F,F1, t1 be natural_transformation of F1,
  F2;
  assume that
A1: F is_naturally_transformable_to F1 and
A2: F1 is_naturally_transformable_to F2 and
A3: F2 is_naturally_transformable_to F3;
A4: F is_naturally_transformable_to F2 by A1,A2,Th8;
  let t3 be natural_transformation of F2,F3;
A5: F2 is_transformable_to F3 by A3;
A6: F is_transformable_to F1 & F1 is_transformable_to F2 by A1,A2;
  F1 is_naturally_transformable_to F3 by A2,A3,Th8;
  hence t3`*`t1`*`t = t3`*`t1`*`(t qua transformation of F,F1) by A1,Def8
    .= (t3 qua transformation of F2,F3)`*`t1`*`t by A2,A3,Def8
    .= t3`*`(t1`*`(t qua transformation of F,F1)) by A6,A5,Th6
    .= (t3 qua transformation of F2,F3)`*`(t1`*`t) by A1,A2,Def8
    .= t3 `*`(t1`*`t) by A3,A4,Def8;
end;

begin :: Category of Functors

definition
  let I be set;
  let A,B be ManySortedSet of I;
  func Funcs(A,B) -> set means
  :Def9:
  for x be set holds x in it iff x is
ManySortedFunction of A,B if for i being set st i in I holds B.i = {} implies A
  .i = {} otherwise it = {};
  existence
  proof
    thus (for i being set st i in I holds B.i = {} implies A.i = {}) implies
ex IT being set st for x be set holds x in IT iff x is ManySortedFunction of A,
    B
    proof
      deffunc F(object) = Funcs(A.$1,B.$1);
      assume
A1:   for i being set st i in I holds B.i = {} implies A.i = {};
      consider F being ManySortedSet of I such that
A2:   for i be object st i in I holds F.i = F(i) from PBOOLE:sch 4;
      take product F;
      let x be set;
      thus x in product F implies x is ManySortedFunction of A,B
      proof
        assume x in product F;
        then consider g be Function such that
A3:     x = g and
A4:     dom g = dom F and
A5:     for i be object st i in dom F holds g.i in F.i by CARD_3:def 5;
A6:     for i be object st i in I holds g.i is Function of A.i,B.i
        proof
          let i be object such that
A7:       i in I;
          dom F = I & F.i = Funcs(A.i,B.i) by A2,A7,PARTFUN1:def 2;
          hence thesis by A5,A7,FUNCT_2:66;
        end;
        dom F = I by PARTFUN1:def 2;
        then reconsider g as ManySortedSet of I by A4,PARTFUN1:def 2
,RELAT_1:def 18;
        g is ManySortedFunction of A,B by A6,PBOOLE:def 15;
        hence thesis by A3;
      end;
      assume
A8:   x is ManySortedFunction of A,B;
      then reconsider g = x as ManySortedSet of I;
A9:   for i be set st i in I holds g.i in Funcs(A.i,B.i)
      proof
        let i be set;
        assume
A10:    i in I;
        then
A11:    B.i = {} implies A.i = {} by A1;
        g.i is Function of A.i, B.i by A8,A10,PBOOLE:def 15;
        hence thesis by A11,FUNCT_2:8;
      end;
A12:  for i be set st i in I holds g.i in F.i
      proof
        let i be set;
        assume
A13:    i in I;
        then F.i = Funcs(A.i,B.i) by A2;
        hence thesis by A9,A13;
      end;
A14:  for i be object st i in dom F holds g.i in F.i
      proof
A15:    dom F = I by PARTFUN1:def 2;
        let i be object;
        assume i in dom F;
        hence thesis by A12,A15;
      end;
      dom g = I by PARTFUN1:def 2;
      then dom g = dom F by PARTFUN1:def 2;
      hence thesis by A14,CARD_3:def 5;
    end;
    thus thesis;
  end;
  uniqueness
  proof
    let it1,it2 be set;
    hereby
      assume for i being set st i in I holds B.i = {} implies A.i = {};
      assume that
A16:  for x being set holds x in it1 iff x is ManySortedFunction of A ,B and
A17:  for x being set holds x in it2 iff x is ManySortedFunction of A ,B;
      now
        let x be object;
        x in it1 iff x is ManySortedFunction of A,B by A16;
        hence x in it1 iff x in it2 by A17;
      end;
      hence it1 = it2 by TARSKI:2;
    end;
    thus thesis;
  end;
  consistency;
end;

definition
  let A,B be transitive with_units non empty AltCatStr;
  func Funct(A,B) -> set means
  :Def10:
  for x being object holds x in it iff x is covariant strict Functor of A,B;
  existence
  proof
    set A9 = Funcs([:the carrier of A,the carrier of A:], [:the carrier of B,
    the carrier of B:]);
    set sAA = the set of all (the Arrows of B)*f where f is Element of A9;
    set f = the Element of A9;
    (the Arrows of B)*f in sAA;
    then reconsider sAA as non empty set;
    defpred R[object,object] means
     ex f be Covariant bifunction of the carrier of A,
the carrier of B, m be MSUnTrans of f, the Arrows of A, the Arrows of B st $1 =
    [f,m] & $2 = FunctorStr (#f,m#) & $2 is covariant Functor of A,B;
    defpred P[object,object] means
      ex AA being ManySortedSet of [:the carrier of A,
    the carrier of A:] st $1 = AA & $2 = Funcs(the Arrows of A, AA);
A1: for x,y,z being object st P[x,y] & P[x,z] holds y = z;
    consider XX being set such that
A2: for x being object holds x in XX iff
     ex y being object st y in sAA & P[y,x] from TARSKI:sch 1(A1);
A3: for x,y,z be object st R[x,y] & R[x,z] holds y = z
    proof
      let x,y,z be object;
      given f be Covariant bifunction of the carrier of A,the carrier of B, m
      be MSUnTrans of f, the Arrows of A, the Arrows of B such that
A4:   x = [f,m] and
A5:   y = FunctorStr (#f,m#) and
      y is covariant Functor of A,B;
      given f1 be Covariant bifunction of the carrier of A,the carrier of B,
      m1 be MSUnTrans of f1, the Arrows of A, the Arrows of B such that
A6:   x = [f1,m1] and
A7:   z = FunctorStr (#f1,m1#) and
      z is covariant Functor of A,B;
      f=f1 by A4,A6,XTUPLE_0:1;
      hence thesis by A4,A5,A6,A7,XTUPLE_0:1;
    end;
    consider X be set such that
A8: for x be object holds x in X iff
     ex y be object st y in [:A9,union XX:] & R[y,x] from TARSKI:sch 1(A3);
   take X;
    let x be object;
    thus x in X implies x is covariant strict Functor of A,B
    proof
      assume x in X;
      then ex y be object st y in [:A9,union XX:] &
       ex f be Covariant bifunction of the carrier of A,the carrier of B,
          m be MSUnTrans of f, the Arrows of A, the Arrows of B
      st y = [f,m] & x = FunctorStr (#f,m#) & x is covariant Functor of A,B
            by A8;
      hence thesis;
    end;
    assume x is covariant strict Functor of A,B;
    then reconsider F = x as covariant strict Functor of A,B;
    reconsider f = the ObjectMap of F as Covariant bifunction of the carrier
    of A,the carrier of B by FUNCTOR0:def 12;
    reconsider m = the MorphMap of F as MSUnTrans of f, the Arrows of A, the
    Arrows of B;
    reconsider y = [f,m] as set by TARSKI:1;
A9: for o1,o2 be Object of A st (the Arrows of A).(o1,o2) <> {} holds (
    the Arrows of B).(f.(o1,o2)) <> {}
    proof
      let o1,o2 be Object of A such that
A10:  (the Arrows of A).(o1,o2) <> {};
      (the Arrows of A).(o1,o2) = <^o1,o2^>;
      hence thesis by A10,FUNCTOR0:def 11;
    end;
A11: for o1,o2 be Object of A st (the Arrows of A).(o1,o2) <> {} holds (
    the Arrows of B).([F.o1,F.o2]) <> {}
    proof
      let o1,o2 be Object of A such that
A12:  (the Arrows of A).(o1,o2) <> {};
      f.(o1,o2) = [F.o1,F.o2] by FUNCTOR0:22;
      hence thesis by A9,A12;
    end;
    y in [:A9,union XX:]
    proof
      set I = [:the carrier of A,the carrier of A:];
      reconsider AA = (the Arrows of B)*f as ManySortedSet of [:the carrier of
      A,the carrier of A:];
A13:  for i be set st i in I & (the Arrows of A).i <> {} holds (the
      Arrows of B).(f.i) <> {}
      proof
        let i be set such that
A14:    i in I and
A15:    (the Arrows of A).i <> {};
        consider o1,o2 be object such that
A16:    o1 in the carrier of A & o2 in the carrier of A and
A17:    i = [o1,o2] by A14,ZFMISC_1:def 2;
        reconsider a1 = o1, a2 = o2 as Object of A by A16;
A18:    (the Arrows of B).(f.i) = (the Arrows of B).(f.(o1,o2)) by A17
          .= (the Arrows of B).([F.a1,F.a2]) by FUNCTOR0:22;
        (the Arrows of A).(o1,o2) <> {} by A15,A17;
        hence thesis by A11,A18;
      end;
      for i be set st i in I holds (the Arrows of A).i <> {} implies AA.i <> {}
      proof
        let i be set such that
A19:    i in I;
        assume
A20:    (the Arrows of A).i <> {};
        AA.i = (the Arrows of B).(f.i) by A19,FUNCT_2:15;
        hence thesis by A13,A19,A20;
      end;
      then m is ManySortedFunction of the Arrows of A,AA & for i be set st i
      in I holds AA.i = {} implies (the Arrows of A). i = {} by FUNCTOR0:def 4;
      then
A21:  m in Funcs(the Arrows of A,AA) by Def9;
A22:  f in A9 by FUNCT_2:8;
      then (the Arrows of B)*f in sAA;
      then Funcs(the Arrows of A,AA) in XX by A2;
      then m in union XX by A21,TARSKI:def 4;
      hence thesis by A22,ZFMISC_1:def 2;
    end;
    hence thesis by A8;
  end;
  uniqueness
  proof
    let it1,it2 be set such that
A23: for x being object holds x in it1 iff x is covariant strict Functor
    of A, B and
A24: for x being object
    holds x in it2 iff x is covariant strict Functor of A,B;
    now
      let x be object;
      x in it1 iff x is covariant strict Functor of A,B by A23;
      hence x in it1 iff x in it2 by A24;
    end;
    hence thesis by TARSKI:2;
  end;
end;

definition
  let A,B be category;
  func Functors(A,B) -> strict non empty transitive AltCatStr means
  the
carrier of it = Funct(A,B) & (for F,G being strict covariant Functor of A,B, x
  being set holds x in (the Arrows of it).(F,G) iff F
is_naturally_transformable_to G & x is natural_transformation of F,G) & for F,G
,H being strict covariant Functor of A,B st F is_naturally_transformable_to G &
  G is_naturally_transformable_to H for t1 being natural_transformation of F,G,
t2 being natural_transformation of G,H ex f being Function st f = (the Comp of
  it).(F,G,H) & f.(t2,t1) = t2`*`t1;
  existence
  proof
    defpred Q[object,object,object] means
    for f,g,h being strict covariant Functor of A
    ,B st [f,g,h] = $3 for t1 being natural_transformation of f,g for t2 being
natural_transformation of g,h st [t2,t1] = $2 & ex v being Function st v.$2 =
    $1 holds $1 = t2 `*` t1;
    defpred P[object,object] means
    ex D2 being set st D2 = $2 &
for f,g being strict covariant Functor of A,B st
[f,g] = $1 for x being set holds x in D2 iff f is_naturally_transformable_to g
    & x is natural_transformation of f,g;
A1: for i being object st i in [:Funct(A,B),Funct(A,B):]
ex j being object st P[ i,j]
    proof
      let i be object;
      assume i in [:Funct(A,B),Funct(A,B):];
      then consider f,g be object such that
A2:   f in Funct(A,B) & g in Funct(A,B) and
A3:   i = [f,g] by ZFMISC_1:def 2;
      reconsider f, g as strict covariant Functor of A,B by A2,Def10;
      defpred P[Object of A,object] means $2 = <^f.$1,g.$1^>;
      defpred P[object] means f is_naturally_transformable_to g & $1 is
      natural_transformation of f,g;
A4:   for a being Element of A ex j being object st P[a,j];
      consider N being ManySortedSet of the carrier of A such that
A5:   for a being Element of A holds P[a,N.a] from PBOOLE:sch 6(A4);
      consider j being set such that
A6:   for x being object holds x in j iff x in product N & P[x] from
      XBOOLE_0:sch 1;
      take j,j;
      thus j=j;
      let f9,g9 be strict covariant Functor of A,B such that
A7:   [f9,g9] = i;
      let x be set;
      thus x in j implies f9 is_naturally_transformable_to g9 & x is
      natural_transformation of f9,g9
      proof
        assume
A8:     x in j;
        f9 = f & g9 = g by A3,A7,XTUPLE_0:1;
        hence thesis by A6,A8;
      end;
      thus f9 is_naturally_transformable_to g9 & x is natural_transformation
      of f9,g9 implies x in j
      proof
A9:     f9 = f & g9 = g by A3,A7,XTUPLE_0:1;
        set I = the carrier of A;
        assume that
A10:    f9 is_naturally_transformable_to g9 and
A11:    x is natural_transformation of f9,g9;
        reconsider h = x as ManySortedSet of the carrier of A by A11;
A12:    f9 is_transformable_to g9 by A10;
A13:    for i9 be set st i9 in I holds h.i9 in N.i9
        proof
          let i9 be set;
          assume i9 in I;
          then reconsider i9 as Element of A;
A14:      P[i9,N.i9] by A5;
          <^f.i9,g.i9^> <> {} & h.i9 is Element of <^f.i9,g.i9^> by A11,A12,A9
,Def2;
          hence thesis by A14;
        end;
A15:    for i9 be object st i9 in dom N holds h.i9 in N.i9
        proof
A16:      dom N = I by PARTFUN1:def 2;
          let i9 be object;
          assume i9 in dom N;
          hence thesis by A13,A16;
        end;
        dom h = the carrier of A by PARTFUN1:def 2;
        then dom h = dom N by PARTFUN1:def 2;
        then x in product N by A15,CARD_3:9;
        hence thesis by A6,A10,A11,A9;
      end;
    end;
    consider a be ManySortedSet of [:Funct(A,B),Funct(A,B):] such that
A17: for i being object st i in [:Funct(A,B),Funct(A,B):] holds P[i,a.i]
    from PBOOLE:sch 3(A1);
A18: for o be object st o in [:Funct(A,B),Funct(A,B),Funct(A,B):]
     for x be object st x in {|a,a|}.o
      ex y be object st y in {|a|}.o & Q[y,x,o]
    proof
      let o be object;
      assume o in [:Funct(A,B),Funct(A,B),Funct(A,B):];
      then o in [:[:Funct(A,B),Funct(A,B):],Funct(A,B):] by ZFMISC_1:def 3;
      then consider ff,h be object such that
A19:  ff in [:Funct(A,B),Funct(A,B):] and
A20:  h in Funct(A,B) and
A21:  o = [ff,h] by ZFMISC_1:def 2;
      consider f,g be object such that
A22:  f in Funct(A,B) & g in Funct(A,B) and
A23:  ff = [f,g] by A19,ZFMISC_1:def 2;
A24:  o = [f,g,h] by A21,A23;
      reconsider T = Funct(A,B) as non empty set by A20;
      reconsider i = f, j = g, k = h as Element of T by A20,A22;
A25:  {|a|}.[i,j,k] = {|a|}.(i,j,k) by MULTOP_1:def 1
        .= a.(i,k) by ALTCAT_1:def 3;
A26:  {|a,a|}.[i,j,k] = {|a,a|}.(i,j,k) by MULTOP_1:def 1
        .= [:a.(j,k),a.(i,j):] by ALTCAT_1:def 4;
      for x be object st x in {|a,a|}.o
      ex y be object st y in {|a|}.o & Q[y,x, o]
      proof
        reconsider i9 = i,j9 = j, k9 = k as strict covariant Functor of A,B by
Def10;
        let x be object;
        assume x in {|a,a|}.o;
        then consider x2,x1 be object such that
A27:    x2 in a.(j,k) and
A28:    x1 in a.(i,j) and
A29:    x = [x2,x1] by A24,A26,ZFMISC_1:def 2;
A30:    x2 in a.[j,k] by A27;
A31:      P[[j,k],a.[j,k]] by A17;
        then
A32:    j9 is_naturally_transformable_to k9 by A30;
        reconsider x2 as natural_transformation of j9,k9 by A30,A31;
A33:    x1 in a.[i,j] by A28;
        P[[i,j],a.[i,j]] by A17;
        then reconsider x1 as natural_transformation of i9,j9 by A33;
        reconsider vv = x2 `*` x1 as natural_transformation of i9,k9;
A34:    for f,g,h being strict covariant Functor of A,B st [f,g,h] = o
for t1 being natural_transformation of f,g for t2 being natural_transformation
of g,h st [t2,t1] = x & ex v being Function st v.x = vv holds vv = t2 `*` t1
        proof
          let f,g,h be strict covariant Functor of A,B such that
A35:      [f,g,h] = o;
A36:      j9 = g by A24,A35,XTUPLE_0:3;
          then reconsider x2 as natural_transformation of g,h by A24,A35,
XTUPLE_0:3;
A37:      i9 = f & k9 = h by A24,A35,XTUPLE_0:3;
          let t1 be natural_transformation of f,g, t2 be
          natural_transformation of g,h such that
A38:      [t2,t1] = x and
          ex v being Function st v.x = vv;
          x2 = t2 by A29,A38,XTUPLE_0:1;
          hence thesis by A29,A38,A36,A37,XTUPLE_0:1;
        end;
        P[[i,j],a.[i,j]] by A17;
        then i9 is_naturally_transformable_to j9 by A33;
        then
A39:       i9 is_naturally_transformable_to k9 by A32,Th8;
        P[[i,k],a.[i,k]] by A17;
        then vv in a.[i9,k9] by A39;
        hence thesis by A24,A25,A34;
      end;
      hence thesis;
    end;
    consider c being ManySortedFunction of {|a,a|},{|a|} such that
A40: for i being object st i in [:Funct(A,B),Funct(A,B),Funct(A,B):]
  ex v being Function of {|a,a|}.i, {|a|}.i st v = c.i &
  for x be object st x
    in {|a,a|}.i holds Q[v.x,x,i] from MSSUBFAM:sch 1(A18);
    set F = AltCatStr (#Funct(A,B),a,c #);
A41: Funct(A,B) is non empty
    proof
      set f = the strict covariant Functor of A,B;
      f in Funct(A,B) by Def10;
      hence thesis;
    end;
    F is transitive
    proof
      let o1,o2,o3 be Object of F;
      reconsider a1 = o1, a2 = o2, a3 = o3 as strict covariant Functor of A,B
      by A41,Def10;
      assume that
A42:  <^o1,o2^> <> {} and
A43:  <^o2,o3^> <> {};
      consider x being object such that
A44:  x in a.[o2,o3] by A43,XBOOLE_0:def 1;
  [o2,o3] in [:Funct(A,B),Funct(A,B):] by A41,ZFMISC_1:def 2;
      then
A45:     P[[o2,o3],a.[o2,o3]] by A17;
      then
A46:  a2 is_naturally_transformable_to a3 by A44;
      reconsider x as natural_transformation of a2,a3 by A44,A45;
      consider y being object such that
A47:  y in a.[o1,o2] by A42,XBOOLE_0:def 1;
  [o1,o2] in [:Funct(A,B),Funct(A,B):] by A41,ZFMISC_1:def 2;
      then
A48:    P[[o1,o2],a.[o1,o2]] by A17;
      then reconsider y as natural_transformation of a1,a2 by A47;
      a1 is_naturally_transformable_to a2 by A47,A48;
      then
A49:  a1 is_naturally_transformable_to a3 by A46,Th8;
A50:   x `*` y is natural_transformation of a1,a3 & [o1,o3] in [:Funct(A,B
      ),Funct(A,B):] by A41,ZFMISC_1:def 2;
      then P[[o1,o3],a.[o1,o3]] by A17;
      hence thesis by A49,A50;
    end;
    then reconsider F as strict non empty transitive AltCatStr by A41;
    take F;
    thus the carrier of F = Funct(A,B);
    thus for f,g being strict covariant Functor of A,B, x being set holds x in
    (the Arrows of F).(f,g) iff f is_naturally_transformable_to g & x is
    natural_transformation of f,g
    proof
      let f,g be strict covariant Functor of A,B;
      let x be set;
      thus x in (the Arrows of F).(f,g) implies f
      is_naturally_transformable_to g & x is natural_transformation of f,g
      proof
        f in Funct(A,B) & g in Funct(A,B) by Def10;
        then
A51:    [f,g] in [:Funct(A,B),Funct(A,B):] by ZFMISC_1:def 2;
        assume
A52:       x in (the Arrows of F).(f,g);
         P[[f,g],a.[f,g]] by A17,A51;
        hence thesis by A52;
      end;
      thus f is_naturally_transformable_to g & x is natural_transformation of
      f,g implies x in (the Arrows of F).(f,g)
      proof
        f in Funct(A,B) & g in Funct(A,B) by Def10;
        then
A53:    [f,g] in [:Funct(A,B),Funct(A,B):] by ZFMISC_1:87;
        assume
A54
:      f is_naturally_transformable_to g & x is natural_transformation of f,g;
         P[[f,g],a.[f,g]] by A17,A53;
        hence thesis by A54;
      end;
    end;
    let f,g,h be strict covariant Functor of A,B such that
A55: f is_naturally_transformable_to g and
A56: g is_naturally_transformable_to h;
    let t1 be natural_transformation of f,g, t2 be natural_transformation of g
    ,h;
A57: f in Funct(A,B) by Def10;
    then reconsider T = Funct(A,B) as non empty set;
A58: g in Funct(A,B) by Def10;
    then
A59: [f,g] in [:Funct(A,B),Funct(A,B):] by A57,ZFMISC_1:87;
A60: h in Funct(A,B) by Def10;
    then [g,h] in [:Funct(A,B),Funct(A,B):] by A58,ZFMISC_1:87;
    then P[[g,h],a.[g,h]] by A17;
    then
A61: t2 in a.[g,h] by A56;
    reconsider i = f, j = g, k = h as Element of T by Def10;
A62: {|a,a|}.[i,j,k] = {|a,a|}.(i,j,k) by MULTOP_1:def 1
      .= [:a.(j,k),a.(i,j):] by ALTCAT_1:def 4;
    [:Funct(A,B),Funct(A,B),Funct(A,B):] = [:[:Funct(A,B),Funct(A,B):],
    Funct(A,B) :] & [f,g,h] = [[f,g],h] by ZFMISC_1:def 3;
    then [f,g,h] in [:Funct(A,B),Funct(A,B),Funct(A,B):] by A60,A59,ZFMISC_1:87
;
    then consider v be Function of {|a,a|}.[f,g,h], {|a|}.[f,g,h] such that
A63: v = c.[f,g,h] and
A64: for x be object st x in {|a,a|}.[f,g,h] holds Q[v.x,x,[f,g,h]] by A40;
    P[[f,g],a.[f,g]] by A17,A59;
    then t1 in a.[f,g] by A55;
    then [t2,t1] in {|a,a|}.[f,g,h] by A62,A61,ZFMISC_1:87;
    then
A65: v.(t2,t1) = t2`*`t1 by A64;
    v = c.(f,g,h) by A63,MULTOP_1:def 1;
    hence thesis by A65;
  end;
  uniqueness
  proof
    let C1,C2 be strict non empty transitive AltCatStr such that
A66: the carrier of C1 = Funct(A,B) and
A67: for F,G being strict covariant Functor of A,B, x being set holds
    x in (the Arrows of C1).(F,G) iff F is_naturally_transformable_to G & x is
    natural_transformation of F,G and
A68: for F,G,H being strict covariant Functor of A,B st F
    is_naturally_transformable_to G & G is_naturally_transformable_to H for t1
being natural_transformation of F,G, t2 being natural_transformation of G,H ex
    f being Function st f = (the Comp of C1).(F,G,H) & f.(t2,t1) = t2`*` t1 and
A69: the carrier of C2 = Funct(A,B) and
A70: for F,G being strict covariant Functor of A,B, x being set holds
    x in (the Arrows of C2).(F,G) iff F is_naturally_transformable_to G & x is
    natural_transformation of F,G and
A71: for F,G,H being strict covariant Functor of A,B st F
    is_naturally_transformable_to G & G is_naturally_transformable_to H for t1
being natural_transformation of F,G, t2 being natural_transformation of G,H ex
    f being Function st f = (the Comp of C2).(F,G,H) & f.(t2,t1) = t2`*`t1;
    set R = the carrier of C1, T = the carrier of C2, N = the Arrows of C1, M
    = the Arrows of C2, O = the Comp of C1, P = the Comp of C2;
A72: for i,j being object st i in R & j in T holds N.(i,j) = M.(i,j)
    proof
      let i,j be object such that
A73:  i in R and
A74:  j in T;
      reconsider g = j as strict covariant Functor of A,B by A69,A74,Def10;
      reconsider f = i as strict covariant Functor of A,B by A66,A73,Def10;
      now
        let x be object;
        x in N.(i,j) iff f is_naturally_transformable_to g & x is
        natural_transformation of f,g by A67;
        hence x in N.(i,j) iff x in M.(i,j) by A70;
      end;
      hence thesis by TARSKI:2;
    end;
    then
A75: the Arrows of C1 = the Arrows of C2 by A66,A69,ALTCAT_1:6;
    for i,j,k being object st i in R & j in R & k in R holds O.(i,j,k) = P.
    (i, j, k )
    proof
      let i,j,k be object;
      assume that
A76:  i in R and
A77:  j in R and
A78:  k in R;
      reconsider h = k as strict covariant Functor of A,B by A66,A78,Def10;
      reconsider g = j as strict covariant Functor of A,B by A66,A77,Def10;
      reconsider f = i as strict covariant Functor of A,B by A66,A76,Def10;
      per cases;
      suppose
A79:    N.(i,j) = {} or N.(j,k) = {};
        thus O.(i,j,k) = P.(i,j,k)
        proof
          per cases by A79;
          suppose
A80:        N.(i,j) = {};
            reconsider T as non empty set;
            reconsider i9 = i, j9 = j, k9 = k as Element of T by A66,A69,A76
,A77,A78;
            M.(i,j) = {} by A66,A69,A72,A80,ALTCAT_1:6;
            then
A81:        [:M.(j9,k9),M.(i9,j9):] = {} by ZFMISC_1:90;
A82:        {|M,M|}.[i9,j9,k9] = {|M,M|}.(i9,j9,k9) by MULTOP_1:def 1
              .= [:M.(j9,k9),M.(i9,j9):] by ALTCAT_1:def 4;
A83:        {|M|}.[i9,j9,k9] = {|M|}.(i9,j9,k9) by MULTOP_1:def 1
              .= M.(i9,k9) by ALTCAT_1:def 3;
            P.[i9,j9,k9] = P.(i9,j9,k9) by MULTOP_1:def 1;
            then
A84:        P.(i9,j9,k9) is Function of [:M.(j9,k9),M.(i9,j9):], M.(i9,
            k9) by A82,A83,PBOOLE:def 15;
A85:        {|M,M|}.[i9,j9,k9] = {|M,M|}.(i9,j9,k9) by MULTOP_1:def 1
              .= [:M.(j9,k9),M.(i9,j9):] by ALTCAT_1:def 4;
A86:        {|M|}.[i9,j9,k9] = {|M|}.(i9,j9,k9) by MULTOP_1:def 1
              .= M.(i9,k9) by ALTCAT_1:def 3;
            O.[i9,j9,k9] = O.(i9,j9,k9) by MULTOP_1:def 1;
            then O.(i9,j9,k9) is Function of [:M.(j9,k9),M.(i9,j9):], M.(i9,
            k9) by A66,A69,A75,A85,A86,PBOOLE:def 15;
            hence thesis by A81,A84;
          end;
          suppose
A87:        N.(j,k) = {};
            reconsider T as non empty set;
            reconsider i9 = i, j9 = j, k9 = k as Element of T by A66,A69,A76
,A77,A78;
            M.(j,k) = {} by A66,A69,A72,A87,ALTCAT_1:6;
            then
A88:        [:M.(j9,k9),M.(i9,j9):] = {} by ZFMISC_1:90;
A89:        {|M,M|}.[i9,j9,k9] = {|M,M|}.(i9,j9,k9) by MULTOP_1:def 1
              .= [:M.(j9,k9),M.(i9,j9):] by ALTCAT_1:def 4;
A90:        {|M|}.[i9,j9,k9] = {|M|}.(i9,j9,k9) by MULTOP_1:def 1
              .= M.(i9,k9) by ALTCAT_1:def 3;
            P.[i9,j9,k9] = P.(i9,j9,k9) by MULTOP_1:def 1;
            then
A91:        P.(i9,j9,k9) is Function of [:M.(j9,k9),M.(i9,j9):], M.(i9,
            k9) by A89,A90,PBOOLE:def 15;
A92:        {|M,M|}.[i9,j9,k9] = {|M,M|}.(i9,j9,k9) by MULTOP_1:def 1
              .= [:M.(j9,k9),M.(i9,j9):] by ALTCAT_1:def 4;
A93:        {|M|}.[i9,j9,k9] = {|M|}.(i9,j9,k9) by MULTOP_1:def 1
              .= M.(i9,k9) by ALTCAT_1:def 3;
            O.[i9,j9,k9] = O.(i9,j9,k9) by MULTOP_1:def 1;
            then O.(i9,j9,k9) is Function of [:M.(j9,k9),M.(i9,j9):], M.(i9,
            k9) by A66,A69,A75,A92,A93,PBOOLE:def 15;
            hence thesis by A88,A91;
          end;
        end;
      end;
      suppose that
A94:    N.(i,j) <> {} and
A95:    N.(j,k) <> {};
        reconsider T as non empty set;
        reconsider i9 = i, j9 = j, k9 = k as Element of T by A66,A69,A76,A77
,A78;
A96:    {|M,M|}.[i9,j9,k9] = {|M,M|}.(i9,j9,k9) by MULTOP_1:def 1
          .= [:M.(j9,k9),M.(i9,j9):] by ALTCAT_1:def 4;
A97:    {|M|}.[i9,j9,k9] = {|M|}.(i9,j9,k9) by MULTOP_1:def 1
          .= M.(i9,k9) by ALTCAT_1:def 3;
        P.[i9,j9,k9] = P.(i9,j9,k9) by MULTOP_1:def 1;
        then reconsider
        t2 = P.(i,j,k) as Function of [:M.(j,k),M.(i,j):], M.(i,k)
        by A96,A97,PBOOLE:def 15;
A98:    {|M,M|}.[i9,j9,k9] = {|M,M|}.(i9,j9,k9) by MULTOP_1:def 1
          .= [:M.(j9,k9),M.(i9,j9):] by ALTCAT_1:def 4;
A99:    {|M|}.[i9,j9,k9] = {|M|}.(i9,j9,k9) by MULTOP_1:def 1
          .= M.(i9,k9) by ALTCAT_1:def 3;
        O.[i9,j9,k9] = O.(i9,j9,k9) by MULTOP_1:def 1;
        then reconsider
        t1 = O.(i,j,k) as Function of [:M.(j,k),M.(i,j):], M.(i,k)
        by A66,A69,A75,A98,A99,PBOOLE:def 15;
A100:    M.(j,k) <> {} by A66,A69,A72,A95,ALTCAT_1:6;
A101:    M.(i,j) <> {} by A66,A69,A72,A94,ALTCAT_1:6;
        for a being Element of M.(j,k) for b being Element of M.(i,j)
        holds t1.(a,b) = t2.(a,b)
        proof
          let a be Element of M.(j,k), b be Element of M.(i,j);
          a in M.(j,k) by A100;
          then
A102:      g is_naturally_transformable_to h by A70;
          reconsider a as natural_transformation of g,h by A70,A100;
          b in M.(i,j) by A101;
          then
A103:      f is_naturally_transformable_to g by A70;
          reconsider b as natural_transformation of f,g by A70,A101;
          (ex t19 be Function st t19 = O.(f,g,h) & t19.(a,b) = a `*` b )
& ex t29 be Function st t29 = P.(f,g,h) & t29.(a,b) = a `*` b by A68,A71,A102
,A103;
          hence thesis;
        end;
        hence thesis by BINOP_1:2;
      end;
    end;
    hence thesis by A66,A69,A75,ALTCAT_1:8;
  end;
end;