:: FUNCTOR2 semantic presentation

begin

registration
let A be non empty transitive with_units AltCatStr ;
let B be non empty with_units AltCatStr ;
cluster  ->  feasible id-preserving for Functor of A,B;
coherence
 for b1 being Functor of A,B holds
( b1 is feasible & b1 is id-preserving ) by FUNCTOR0:def_25;
end;

registration
let A be non empty transitive with_units AltCatStr ;
let B be non empty with_units AltCatStr ;
cluster covariant  ->  Covariant comp-preserving for Functor of A,B;
coherence
 for b1 being Functor of A,B st b1 is covariant holds
( b1 is Covariant & b1 is comp-preserving ) by FUNCTOR0:def_26;
cluster Covariant comp-preserving  ->  covariant for Functor of A,B;
coherence
 for b1 being Functor of A,B st b1 is Covariant & b1 is comp-preserving holds
b1 is covariant by FUNCTOR0:def_26;
cluster contravariant  ->  Contravariant comp-reversing for Functor of A,B;
coherence
 for b1 being Functor of A,B st b1 is contravariant holds
( b1 is Contravariant & b1 is comp-reversing ) by FUNCTOR0:def_27;
cluster Contravariant comp-reversing  ->  contravariant for Functor of A,B;
coherence
 for b1 being Functor of A,B st b1 is Contravariant & b1 is comp-reversing holds
b1 is contravariant by FUNCTOR0:def_27;
end;

theorem Th1: :: FUNCTOR2:1
for A, B being non empty transitive with_units AltCatStr
for 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 non empty transitive with_units AltCatStr ; ::_thesis: for F being covariant Functor of A,B
for a being object of A holds F . (idm a) = idm (F . a)
let F be covariant Functor of A,B; ::_thesis: for a being object of A holds F . (idm a) = idm (F . a)
let a be object of A; ::_thesis: F . (idm a) = idm (F . 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 ;
::_thesis: verum
end;

begin

definition
let A, B be non empty transitive with_units AltCatStr ;
let F1, F2 be Functor of A,B;
predF1 is_transformable_to F2 means :Def1: :: FUNCTOR2:def 1
 for a being object of A holds <^(F1 . a),(F2 . a)^> <> {} ;
reflexivity
 for F1 being Functor of A,B
for a being object of A holds <^(F1 . a),(F1 . a)^> <> {} by ALTCAT_2:def_7;
end;

:: deftheorem Def1 defines is_transformable_to FUNCTOR2:def_1_:_
 for A, B being non empty transitive with_units AltCatStr
for F1, F2 being Functor of A,B holds
( F1 is_transformable_to F2 iff for a being object of A holds <^(F1 . a),(F2 . a)^> <> {} );

theorem Th2: :: FUNCTOR2:2
for A, B being non empty transitive with_units AltCatStr
for F, F1, F2 being Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 holds
F is_transformable_to F2
proof
let A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F, F1, F2 being Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 holds
F is_transformable_to F2
let F, F1, F2 be Functor of A,B; ::_thesis: ( F is_transformable_to F1 & F1 is_transformable_to F2 implies F is_transformable_to F2 )
assume A1: ( F is_transformable_to F1 & F1 is_transformable_to F2 ) ; ::_thesis: F is_transformable_to F2
let a be object of A; :: according to FUNCTOR2:def_1 ::_thesis: <^(F . a),(F2 . a)^> <> {}
 ( <^(F . a),(F1 . a)^> <> {} & <^(F1 . a),(F2 . a)^> <> {} ) by A1, Def1;
hence  <^(F . a),(F2 . a)^> <> {} by ALTCAT_1:def_2; ::_thesis: verum
end;

definition
let A, B be non empty transitive with_units AltCatStr ;
let 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: :: FUNCTOR2:def 2
 for a being object of A holds it . a is Morphism of (F1 . a),(F2 . a);
existence
 ex b1 being ManySortedSet of the carrier of A st
for a being object of A holds b1 . a is Morphism of (F1 . a),(F2 . a)
proof
defpred S1[ object of A, set ] means $2 in <^(F1 . $1),(F2 . $1)^>;
A2: for a being Element of A ex j being set st S1[a,j]
proof
let a be Element of A; ::_thesis: ex j being set st S1[a,j]
reconsider o = a as object of A ;
 <^(F1 . o),(F2 . o)^> <> {} by A1, Def1;
hence  ex j being set st S1[a,j] by XBOOLE_0:def_1; ::_thesis: verum
end;
consider t being ManySortedSet of the carrier of A such that
A3: for a being Element of A holds S1[a,t . a] from PBOOLE:sch_6(A2);
take  t ; ::_thesis: for a being object of A holds t . a is Morphism of (F1 . a),(F2 . a)
thus  for a being object of A holds t . a is Morphism of (F1 . a),(F2 . a) by A3; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines transformation FUNCTOR2:def_2_:_
 for A, B being non empty transitive with_units AltCatStr
for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds
for b5 being ManySortedSet of the carrier of A holds
( b5 is transformation of F1,F2 iff for a being object of A holds b5 . a is Morphism of (F1 . a),(F2 . a) );

definition
let A, B be non empty transitive with_units AltCatStr ;
let F be Functor of A,B;
func idt F ->  transformation of F,F means :Def3: :: FUNCTOR2:def 3
 for a being object of A holds it . a = idm (F . a);
existence
 ex b1 being transformation of F,F st
for a being object of A holds b1 . a = idm (F . a)
proof
defpred S1[ object of A, set ] means $2 = idm (F . $1);
A1: for a being Element of A ex j being set st S1[a,j] ;
consider t being ManySortedSet of the carrier of A such that
A2: for a being Element of A holds S1[a,t . a] from PBOOLE:sch_6(A1);
 for a being object of A holds t . a is Morphism of (F . a),(F . a)
proof
let a be Element of A; ::_thesis: t . a is Morphism of (F . a),(F . a)
 S1[a,t . a] by A2;
hence  t . a is Morphism of (F . a),(F . a) ; ::_thesis: verum
end;
then  t is transformation of F,F by Def2;
hence  ex b1 being transformation of F,F st
for a being object of A holds b1 . a = idm (F . a) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being transformation of F,F st ( for a being object of A holds b1 . a = idm (F . a) ) & ( for a being object of A holds b2 . a = idm (F . a) ) holds
b1 = b2
proof
let it1, it2 be transformation of F,F; ::_thesis: ( ( for a being object of A holds it1 . a = idm (F . a) ) & ( for a being object of A holds it2 . a = idm (F . a) ) implies it1 = it2 )
assume 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) ; ::_thesis: it1 = it2
now__::_thesis:_for_a_being_set_st_a_in_the_carrier_of_A_holds_
it1_._a_=_it2_._a
let a be set ; ::_thesis: ( a in the carrier of A implies it1 . a = it2 . a )
assume  a in the carrier of A ; ::_thesis: it1 . a = it2 . a
then reconsider o = a as object of A ;
thus it1 . a = idm (F . o) by A3
.= it2 . a by A4 ; ::_thesis: verum
end;
hence  it1 = it2 by PBOOLE:3; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines idt FUNCTOR2:def_3_:_
 for A, B being non empty transitive with_units AltCatStr
for F being Functor of A,B
for b4 being transformation of F,F holds
( b4 = idt F iff for a being object of A holds b4 . a = idm (F . a) );

definition
let A, B be non empty transitive with_units AltCatStr ;
let 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;
funct ! a ->  Morphism of (F1 . a),(F2 . a) means :Def4: :: FUNCTOR2:def 4
it = t . a;
existence
 ex b1 being Morphism of (F1 . a),(F2 . a) st b1 = t . a
proof
 t . a is Morphism of (F1 . a),(F2 . a) by A1, Def2;
hence  ex b1 being Morphism of (F1 . a),(F2 . a) st b1 = t . a ; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being Morphism of (F1 . a),(F2 . a) st b1 = t . a & b2 = t . a holds
b1 = b2;
;
end;

:: deftheorem Def4 defines ! FUNCTOR2:def_4_:_
 for A, B being non empty transitive with_units AltCatStr
for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds
for t being transformation of F1,F2
for a being object of A
for b7 being Morphism of (F1 . a),(F2 . a) holds
( b7 = t ! a iff b7 = t . a );

definition
let A, B be non empty transitive with_units AltCatStr ;
let 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;
funct2 `*` t1 ->  transformation of F,F2 means :Def5: :: FUNCTOR2:def 5
 for a being object of A holds it ! a = (t2 ! a) * (t1 ! a);
existence
 ex b1 being transformation of F,F2 st
for a being object of A holds b1 ! a = (t2 ! a) * (t1 ! a)
proof
defpred S1[ object of A, set ] means $2 = (t2 ! $1) * (t1 ! $1);
A2: for a being Element of A ex j being set st S1[a,j] ;
consider t being ManySortedSet of the carrier of A such that
A3: for a being Element of A holds S1[a,t . a] from PBOOLE:sch_6(A2);
A4: F is_transformable_to F2 by A1, Th2;
 for a being object of A holds t . a is Morphism of (F . a),(F2 . a)
proof
let o be Element of A; ::_thesis: t . o is Morphism of (F . o),(F2 . o)
 S1[o,t . o] by A3;
hence  t . o is Morphism of (F . o),(F2 . o) ; ::_thesis: verum
end;
then reconsider t9 = t as transformation of F,F2 by A4, Def2;
take  t9 ; ::_thesis: for a being object of A holds t9 ! a = (t2 ! a) * (t1 ! a)
let a be Element of A; ::_thesis: t9 ! a = (t2 ! a) * (t1 ! a)
 S1[a,t . a] by A3;
hence  t9 ! a = (t2 ! a) * (t1 ! a) by A4, Def4; ::_thesis: verum
end;
uniqueness
 for b1, b2 being transformation of F,F2 st ( for a being object of A holds b1 ! a = (t2 ! a) * (t1 ! a) ) & ( for a being object of A holds b2 ! a = (t2 ! a) * (t1 ! a) ) holds
b1 = b2
proof
let it1, it2 be transformation of F,F2; ::_thesis: ( ( for a being object of A holds it1 ! a = (t2 ! a) * (t1 ! a) ) & ( for a being object of A holds it2 ! a = (t2 ! a) * (t1 ! a) ) implies it1 = it2 )
assume 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) ; ::_thesis: it1 = it2
A7: F is_transformable_to F2 by A1, Th2;
now__::_thesis:_for_a_being_set_st_a_in_the_carrier_of_A_holds_
it1_._a_=_it2_._a
let a be set ; ::_thesis: ( a in the carrier of A implies it1 . a = it2 . a )
assume  a in the carrier of A ; ::_thesis: it1 . a = it2 . a
then reconsider o = a as object of A ;
thus it1 . a = it1 ! o by A7, Def4
.= (t2 ! o) * (t1 ! o) by A5
.= it2 ! o by A6
.= it2 . a by A7, Def4 ; ::_thesis: verum
end;
hence  it1 = it2 by PBOOLE:3; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines `*` FUNCTOR2:def_5_:_
 for A, B being non empty transitive with_units AltCatStr
for F, F1, F2 being Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 holds
for t1 being transformation of F,F1
for t2 being transformation of F1,F2
for b8 being transformation of F,F2 holds
( b8 = t2 `*` t1 iff for a being object of A holds b8 ! a = (t2 ! a) * (t1 ! a) );

theorem Th3: :: FUNCTOR2:3
for A, B being non empty transitive with_units AltCatStr
for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds
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 non empty transitive with_units AltCatStr ; ::_thesis: for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds
for t1, t2 being transformation of F1,F2 st ( for a being object of A holds t1 ! a = t2 ! a ) holds
t1 = t2
let F1, F2 be Functor of A,B; ::_thesis: ( 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 )
assume A1: F1 is_transformable_to F2 ; ::_thesis: for t1, t2 being transformation of F1,F2 st ( for a being object of A holds t1 ! a = t2 ! a ) holds
t1 = t2
let t1, t2 be transformation of F1,F2; ::_thesis: ( ( for a being object of A holds t1 ! a = t2 ! a ) implies t1 = t2 )
assume A2: for a being object of A holds t1 ! a = t2 ! a ; ::_thesis: t1 = t2
now__::_thesis:_for_a_being_set_st_a_in_the_carrier_of_A_holds_
t1_._a_=_t2_._a
let a be set ; ::_thesis: ( a in the carrier of A implies t1 . a = t2 . a )
assume  a in the carrier of A ; ::_thesis: t1 . a = t2 . a
then reconsider o = a as object of A ;
thus t1 . a = t1 ! o by A1, Def4
.= t2 ! o by A2
.= t2 . a by A1, Def4 ; ::_thesis: verum
end;
hence  t1 = t2 by PBOOLE:3; ::_thesis: verum
end;

theorem Th4: :: FUNCTOR2:4
for A, B being non empty transitive with_units AltCatStr
for F being Functor of A,B
for a being object of A holds (idt F) ! a = idm (F . a)
proof
let A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F being Functor of A,B
for a being object of A holds (idt F) ! a = idm (F . a)
let F be Functor of A,B; ::_thesis: for a being object of A holds (idt F) ! a = idm (F . a)
let a be object of A; ::_thesis: (idt F) ! a = idm (F . a)
thus (idt F) ! a = (idt F) . a by Def4
.= idm (F . a) by Def3 ; ::_thesis: verum
end;

theorem Th5: :: FUNCTOR2:5
for A, B being non empty transitive with_units AltCatStr
for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds
for t being transformation of F1,F2 holds
( (idt F2) `*` t = t & t `*` (idt F1) = t )
proof
let A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds
for t being transformation of F1,F2 holds
( (idt F2) `*` t = t & t `*` (idt F1) = t )
let F1, F2 be Functor of A,B; ::_thesis: ( F1 is_transformable_to F2 implies for t being transformation of F1,F2 holds
( (idt F2) `*` t = t & t `*` (idt F1) = t ) )
assume A1: F1 is_transformable_to F2 ; ::_thesis: for t being transformation of F1,F2 holds
( (idt F2) `*` t = t & t `*` (idt F1) = t )
let t be transformation of F1,F2; ::_thesis: ( (idt F2) `*` t = t & t `*` (idt F1) = t )
now__::_thesis:_for_a_being_object_of_A_holds_((idt_F2)_`*`_t)_!_a_=_t_!_a
let a be object of A; ::_thesis: ((idt F2) `*` t) ! a = t ! a
A2: <^(F1 . a),(F2 . a)^> <> {} by A1, Def1;
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 ; ::_thesis: verum
end;
hence  (idt F2) `*` t = t by A1, Th3; ::_thesis: t `*` (idt F1) = t
now__::_thesis:_for_a_being_object_of_A_holds_(t_`*`_(idt_F1))_!_a_=_t_!_a
let a be object of A; ::_thesis: (t `*` (idt F1)) ! a = t ! a
A3: <^(F1 . a),(F2 . a)^> <> {} by A1, Def1;
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 ; ::_thesis: verum
end;
hence  t `*` (idt F1) = t by A1, Th3; ::_thesis: verum
end;

theorem Th6: :: FUNCTOR2:6
for A, B being category
for F, F1, F2, F3 being Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 & F2 is_transformable_to F3 holds
for t1 being transformation of F,F1
for t2 being transformation of F1,F2
for t3 being transformation of F2,F3 holds (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1)
proof
let A, B be category; ::_thesis: for F, F1, F2, F3 being Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 & F2 is_transformable_to F3 holds
for t1 being transformation of F,F1
for t2 being transformation of F1,F2
for t3 being transformation of F2,F3 holds (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1)
let F, F1, F2, F3 be Functor of A,B; ::_thesis: ( F is_transformable_to F1 & F1 is_transformable_to F2 & F2 is_transformable_to F3 implies for t1 being transformation of F,F1
for t2 being transformation of F1,F2
for t3 being transformation of F2,F3 holds (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1) )
assume that
A1: F is_transformable_to F1 and
A2: F1 is_transformable_to F2 and
A3: F2 is_transformable_to F3 ; ::_thesis: for t1 being transformation of F,F1
for t2 being transformation of F1,F2
for t3 being transformation of F2,F3 holds (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1)
let t1 be transformation of F,F1; ::_thesis: for t2 being transformation of F1,F2
for t3 being transformation of F2,F3 holds (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1)
let t2 be transformation of F1,F2; ::_thesis: for t3 being transformation of F2,F3 holds (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1)
let t3 be transformation of F2,F3; ::_thesis: (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1)
A4: F1 is_transformable_to F3 by A2, A3, Th2;
A5: F is_transformable_to F2 by A1, A2, Th2;
now__::_thesis:_for_a_being_object_of_A_holds_((t3_`*`_t2)_`*`_t1)_!_a_=_(t3_`*`_(t2_`*`_t1))_!_a
let a be object of A; ::_thesis: ((t3 `*` t2) `*` t1) ! a = (t3 `*` (t2 `*` t1)) ! a
A6: <^(F2 . a),(F3 . a)^> <> {} by A3, Def1;
A7: ( <^(F . a),(F1 . a)^> <> {} & <^(F1 . a),(F2 . a)^> <> {} ) by A1, A2, Def1;
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 ; ::_thesis: verum
end;
hence  (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1) by A1, A4, Th2, Th3; ::_thesis: verum
end;

begin

Lm1:  for A, B being non empty transitive with_units AltCatStr
for F, G being covariant Functor of A,B
for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds ((idt F) ! b) * (F . f) = (F . f) * ((idt F) ! a)
proof
let A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F, G being covariant Functor of A,B
for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds ((idt F) ! b) * (F . f) = (F . f) * ((idt F) ! a)
let F, G be covariant Functor of A,B; ::_thesis: for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds ((idt F) ! b) * (F . f) = (F . f) * ((idt F) ! a)
let a, b be object of A; ::_thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds ((idt F) ! b) * (F . f) = (F . f) * ((idt F) ! a) )
assume A1: <^a,b^> <> {} ; ::_thesis: for f being Morphism of a,b holds ((idt F) ! b) * (F . f) = (F . f) * ((idt F) ! a)
let f be Morphism of a,b; ::_thesis: ((idt F) ! b) * (F . f) = (F . f) * ((idt F) ! a)
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 ; ::_thesis: verum
end;

definition
let A, B be non empty transitive with_units AltCatStr ;
let F1, F2 be covariant Functor of A,B;
predF1 is_naturally_transformable_to F2 means :Def6: :: FUNCTOR2:def 6
( F1 is_transformable_to F2 & ex t being transformation of F1,F2 st
for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (t ! b) * (F1 . f) = (F2 . f) * (t ! a) );
reflexivity
 for F1 being covariant Functor of A,B holds
( F1 is_transformable_to F1 & ex t being transformation of F1,F1 st
for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (t ! b) * (F1 . f) = (F1 . f) * (t ! a) )
proof
let F be covariant Functor of A,B; ::_thesis: ( F is_transformable_to F & ex t being transformation of F,F st
for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (t ! b) * (F . f) = (F . f) * (t ! a) )
thus  F is_transformable_to F ; ::_thesis: ex t being transformation of F,F st
for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (t ! b) * (F . f) = (F . f) * (t ! a)
take  idt F ; ::_thesis: for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds ((idt F) ! b) * (F . f) = (F . f) * ((idt F) ! a)
thus  for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds ((idt F) ! b) * (F . f) = (F . f) * ((idt F) ! a) by Lm1; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines is_naturally_transformable_to FUNCTOR2:def_6_:_
 for A, B being non empty transitive with_units AltCatStr
for F1, F2 being covariant Functor of A,B holds
( F1 is_naturally_transformable_to F2 iff ( F1 is_transformable_to F2 & ex t being transformation of F1,F2 st
for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (t ! b) * (F1 . f) = (F2 . f) * (t ! a) ) );

theorem :: FUNCTOR2:7
for A, B being non empty transitive with_units AltCatStr
for F being covariant Functor of A,B holds F is_naturally_transformable_to F ;

Lm2:  for A, B being category
for F, F1, F2 being covariant Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 holds
for t1 being transformation of F,F1 st ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (t1 ! b) * (F . f) = (F1 . f) * (t1 ! a) ) holds
for t2 being transformation of F1,F2 st ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (t2 ! b) * (F1 . f) = (F2 . f) * (t2 ! a) ) holds
for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds ((t2 `*` t1) ! b) * (F . f) = (F2 . f) * ((t2 `*` t1) ! a)
proof
let A, B be category; ::_thesis: for F, F1, F2 being covariant Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 holds
for t1 being transformation of F,F1 st ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (t1 ! b) * (F . f) = (F1 . f) * (t1 ! a) ) holds
for t2 being transformation of F1,F2 st ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (t2 ! b) * (F1 . f) = (F2 . f) * (t2 ! a) ) holds
for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds ((t2 `*` t1) ! b) * (F . f) = (F2 . f) * ((t2 `*` t1) ! a)
let F, F1, F2 be covariant Functor of A,B; ::_thesis: ( 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^> <> {} holds
for f being Morphism of a,b holds (t1 ! b) * (F . f) = (F1 . f) * (t1 ! a) ) holds
for t2 being transformation of F1,F2 st ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (t2 ! b) * (F1 . f) = (F2 . f) * (t2 ! a) ) holds
for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds ((t2 `*` t1) ! b) * (F . f) = (F2 . f) * ((t2 `*` t1) ! a) )
assume that
A1: F is_transformable_to F1 and
A2: F1 is_transformable_to F2 ; ::_thesis: for t1 being transformation of F,F1 st ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (t1 ! b) * (F . f) = (F1 . f) * (t1 ! a) ) holds
for t2 being transformation of F1,F2 st ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (t2 ! b) * (F1 . f) = (F2 . f) * (t2 ! a) ) holds
for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds ((t2 `*` t1) ! b) * (F . f) = (F2 . f) * ((t2 `*` t1) ! a)
let t1 be transformation of F,F1; ::_thesis: ( ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (t1 ! b) * (F . f) = (F1 . f) * (t1 ! a) ) implies for t2 being transformation of F1,F2 st ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (t2 ! b) * (F1 . f) = (F2 . f) * (t2 ! a) ) holds
for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds ((t2 `*` t1) ! b) * (F . f) = (F2 . f) * ((t2 `*` t1) ! a) )
assume A3: for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (t1 ! b) * (F . f) = (F1 . f) * (t1 ! a) ; ::_thesis: for t2 being transformation of F1,F2 st ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (t2 ! b) * (F1 . f) = (F2 . f) * (t2 ! a) ) holds
for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds ((t2 `*` t1) ! b) * (F . f) = (F2 . f) * ((t2 `*` t1) ! a)
let t2 be transformation of F1,F2; ::_thesis: ( ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (t2 ! b) * (F1 . f) = (F2 . f) * (t2 ! a) ) implies for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds ((t2 `*` t1) ! b) * (F . f) = (F2 . f) * ((t2 `*` t1) ! a) )
assume A4: for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (t2 ! b) * (F1 . f) = (F2 . f) * (t2 ! a) ; ::_thesis: for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds ((t2 `*` t1) ! b) * (F . f) = (F2 . f) * ((t2 `*` t1) ! a)
let a, b be object of A; ::_thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds ((t2 `*` t1) ! b) * (F . f) = (F2 . f) * ((t2 `*` t1) ! a) )
A5: <^(F . b),(F1 . b)^> <> {} by A1, Def1;
A6: <^(F . a),(F1 . a)^> <> {} by A1, Def1;
A7: <^(F1 . b),(F2 . b)^> <> {} by A2, Def1;
A8: <^(F1 . a),(F2 . a)^> <> {} by A2, Def1;
assume A9: <^a,b^> <> {} ; ::_thesis: for f being Morphism of a,b holds ((t2 `*` t1) ! b) * (F . f) = (F2 . f) * ((t2 `*` t1) ! a)
then A10: <^(F . a),(F . b)^> <> {} by FUNCTOR0:def_18;
let f be Morphism of a,b; ::_thesis: ((t2 `*` t1) ! b) * (F . f) = (F2 . f) * ((t2 `*` t1) ! a)
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 ; ::_thesis: verum
end;

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

definition
let A, B be non empty transitive with_units AltCatStr ;
let 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: :: FUNCTOR2:def 7
 for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (it ! b) * (F1 . f) = (F2 . f) * (it ! a);
existence
 ex b1 being transformation of F1,F2 st
for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (b1 ! b) * (F1 . f) = (F2 . f) * (b1 ! a) by A1, Def6;
end;

:: deftheorem Def7 defines natural_transformation FUNCTOR2:def_7_:_
 for A, B being non empty transitive with_units AltCatStr
for F1, F2 being covariant Functor of A,B st F1 is_naturally_transformable_to F2 holds
for b5 being transformation of F1,F2 holds
( b5 is natural_transformation of F1,F2 iff for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (b5 ! b) * (F1 . f) = (F2 . f) * (b5 ! a) );

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

definition
let A, B be category;
let F, F1, F2 be covariant Functor of A,B;
assume B1: ( 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;
funct2 `*` t1 ->  natural_transformation of F,F2 means :Def8: :: FUNCTOR2:def 8
it = t2 `*` t1;
existence
 ex b1 being natural_transformation of F,F2 st b1 = t2 `*` t1
proof
A1: F is_naturally_transformable_to F2 by B1, Th8;
A2: ( ( for a, b being object of A st <^a,b^> <> {} holds
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^> <> {} holds
for f being Morphism of a,b holds (t2 ! b) * (F1 . f) = (F2 . f) * (t2 ! a) ) ) by B1, Def7;
 ( F is_transformable_to F1 & F1 is_transformable_to F2 ) by B1, Def6;
then  for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds ((t2 `*` t1) ! b) * (F . f) = (F2 . f) * ((t2 `*` t1) ! a) by A2, Lm2;
then  t2 `*` t1 is natural_transformation of F,F2 by A1, Def7;
hence  ex b1 being natural_transformation of F,F2 st b1 = t2 `*` t1 ; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being natural_transformation of F,F2 st b1 = t2 `*` t1 & b2 = t2 `*` t1 holds
b1 = b2;
;
end;

:: deftheorem Def8 defines `*` FUNCTOR2:def_8_:_
 for A, B being category
for F, F1, F2 being covariant Functor of A,B st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 holds
for t1 being natural_transformation of F,F1
for t2 being natural_transformation of F1,F2
for b8 being natural_transformation of F,F2 holds
( b8 = t2 `*` t1 iff b8 = t2 `*` t1 );

theorem :: FUNCTOR2:9
for A, B being non empty transitive with_units AltCatStr
for F1, F2 being covariant Functor of A,B st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds
( (idt F2) `*` t = t & t `*` (idt F1) = t )
proof
let A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F1, F2 being covariant Functor of A,B st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds
( (idt F2) `*` t = t & t `*` (idt F1) = t )
let F1, F2 be covariant Functor of A,B; ::_thesis: ( F1 is_naturally_transformable_to F2 implies for t being natural_transformation of F1,F2 holds
( (idt F2) `*` t = t & t `*` (idt F1) = t ) )
assume  F1 is_naturally_transformable_to F2 ; ::_thesis: for t being natural_transformation of F1,F2 holds
( (idt F2) `*` t = t & t `*` (idt F1) = t )
then A1: F1 is_transformable_to F2 by Def6;
let t be natural_transformation of F1,F2; ::_thesis: ( (idt F2) `*` t = t & t `*` (idt F1) = t )
thus  (idt F2) `*` t = t by A1, Th5; ::_thesis: t `*` (idt F1) = t
thus  t `*` (idt F1) = t by A1, Th5; ::_thesis: verum
end;

theorem :: FUNCTOR2:10
for A, B being non empty transitive with_units AltCatStr
for F, F1, F2 being covariant Functor of A,B st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 holds
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)
proof
let A, B be non empty transitive with_units AltCatStr ; ::_thesis: for F, F1, F2 being covariant Functor of A,B st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 holds
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)
let F, F1, F2 be covariant Functor of A,B; ::_thesis: ( 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) )
assume A1: ( F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 ) ; ::_thesis: 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)
let t1 be natural_transformation of F,F1; ::_thesis: for t2 being natural_transformation of F1,F2
for a being object of A holds (t2 `*` t1) ! a = (t2 ! a) * (t1 ! a)
let t2 be natural_transformation of F1,F2; ::_thesis: for a being object of A holds (t2 `*` t1) ! a = (t2 ! a) * (t1 ! a)
let a be object of A; ::_thesis: (t2 `*` t1) ! a = (t2 ! a) * (t1 ! a)
 ( F is_transformable_to F1 & F1 is_transformable_to F2 ) by A1, Def6;
hence  (t2 `*` t1) ! a = (t2 ! a) * (t1 ! a) by Def5; ::_thesis: verum
end;

theorem :: FUNCTOR2:11
for A, B being category
for F, F1, F2, F3 being covariant Functor of A,B
for t being natural_transformation of F,F1
for t1 being natural_transformation of F1,F2 st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds
for t3 being natural_transformation of F2,F3 holds (t3 `*` t1) `*` t = t3 `*` (t1 `*` t)
proof
let A, B be category; ::_thesis: for F, F1, F2, F3 being covariant Functor of A,B
for t being natural_transformation of F,F1
for t1 being natural_transformation of F1,F2 st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds
for t3 being natural_transformation of F2,F3 holds (t3 `*` t1) `*` t = t3 `*` (t1 `*` t)
let F, F1, F2, F3 be covariant Functor of A,B; ::_thesis: for t being natural_transformation of F,F1
for t1 being natural_transformation of F1,F2 st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds
for t3 being natural_transformation of F2,F3 holds (t3 `*` t1) `*` t = t3 `*` (t1 `*` t)
let t be natural_transformation of F,F1; ::_thesis: for t1 being natural_transformation of F1,F2 st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds
for t3 being natural_transformation of F2,F3 holds (t3 `*` t1) `*` t = t3 `*` (t1 `*` t)
let t1 be natural_transformation of F1,F2; ::_thesis: ( 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) )
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 ; ::_thesis: for t3 being natural_transformation of F2,F3 holds (t3 `*` t1) `*` t = t3 `*` (t1 `*` t)
A4: F is_naturally_transformable_to F2 by A1, A2, Th8;
let t3 be natural_transformation of F2,F3; ::_thesis: (t3 `*` t1) `*` t = t3 `*` (t1 `*` t)
A5: F2 is_transformable_to F3 by A3, Def6;
A6: ( F is_transformable_to F1 & F1 is_transformable_to F2 ) by A1, A2, Def6;
 F1 is_naturally_transformable_to F3 by A2, A3, Th8;
hence (t3 `*` t1) `*` t = (t3 `*` t1) `*` t by A1, Def8
.= (t3 `*` t1) `*` t by A2, A3, Def8
.= t3 `*` (t1 `*` t) by A6, A5, Th6
.= t3 `*` (t1 `*` t) by A1, A2, Def8
.= t3 `*` (t1 `*` t) by A3, A4, Def8 ;
::_thesis: verum
end;

begin

definition
let I be set ;
let A, B be ManySortedSet of I;
func Funcs (A,B) ->  set  means :Def9: :: FUNCTOR2:def 9
 for x being set holds
( x in it iff x is ManySortedFunction of A,B ) if  for i being set st i in I & B . i = {} holds
A . i = {}
otherwise it = {} ;
existence
 ( ( ( for i being set st i in I & B . i = {} holds
A . i = {} ) implies ex b1 being set st
for x being set holds
( x in b1 iff x is ManySortedFunction of A,B ) ) & ( ex i being set st
( i in I & B . i = {} & not A . i = {} ) implies ex b1 being set st b1 = {} ) )
proof
thus  ( ( for i being set st i in I & B . i = {} holds
A . i = {} ) implies ex IT being set st
for x being set holds
( x in IT iff x is ManySortedFunction of A,B ) ) ::_thesis: ( ex i being set st
( i in I & B . i = {} & not A . i = {} ) implies ex b1 being set st b1 = {} )
proof
deffunc H1( set ) ->  set = Funcs ((A . $1),(B . $1));
assume A1: for i being set st i in I & B . i = {} holds
A . i = {} ; ::_thesis: ex IT being set st
for x being set holds
( x in IT iff x is ManySortedFunction of A,B )
consider F being ManySortedSet of I such that
A2: for i being set st i in I holds
F . i = H1(i) from PBOOLE:sch_4();
take  product F ; ::_thesis: for x being set holds
( x in product F iff x is ManySortedFunction of A,B )
let x be set ; ::_thesis: ( x in product F iff x is ManySortedFunction of A,B )
thus  ( x in product F implies x is ManySortedFunction of A,B ) ::_thesis: ( x is ManySortedFunction of A,B implies x in product F )
proof
assume  x in product F ; ::_thesis: x is ManySortedFunction of A,B
then consider g being Function such that
A3: x = g and
A4: dom g = dom F and
A5: for i being set st i in dom F holds
g . i in F . i by CARD_3:def_5;
A6: for i being set st i in I holds
g . i is Function of (A . i),(B . i)
proof
let i be set ; ::_thesis: ( i in I implies g . i is Function of (A . i),(B . i) )
assume A7: i in I ; ::_thesis: g . i is Function of (A . i),(B . i)
 ( dom F = I & F . i = Funcs ((A . i),(B . i)) ) by A2, A7, PARTFUN1:def_2;
hence  g . i is Function of (A . i),(B . i) by A5, A7, FUNCT_2:66; ::_thesis: verum
end;
 dom F = I by PARTFUN1:def_2;
then reconsider g = 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  x is ManySortedFunction of A,B by A3; ::_thesis: verum
end;
assume A8: x is ManySortedFunction of A,B ; ::_thesis: x in product F
then reconsider g = x as ManySortedSet of I ;
A9: for i being set st i in I holds
g . i in Funcs ((A . i),(B . i))
proof
let i be set ; ::_thesis: ( i in I implies g . i in Funcs ((A . i),(B . i)) )
assume A10: i in I ; ::_thesis: g . i in Funcs ((A . i),(B . 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  g . i in Funcs ((A . i),(B . i)) by A11, FUNCT_2:8; ::_thesis: verum
end;
A12: for i being set st i in I holds
g . i in F . i
proof
let i be set ; ::_thesis: ( i in I implies g . i in F . i )
assume A13: i in I ; ::_thesis: g . i in F . i
then  F . i = Funcs ((A . i),(B . i)) by A2;
hence  g . i in F . i by A9, A13; ::_thesis: verum
end;
A14: for i being set st i in dom F holds
g . i in F . i
proof
A15: dom F = I by PARTFUN1:def_2;
let i be set ; ::_thesis: ( i in dom F implies g . i in F . i )
assume  i in dom F ; ::_thesis: g . i in F . i
hence  g . i in F . i by A12, A15; ::_thesis: verum
end;
 dom g = I by PARTFUN1:def_2;
then  dom g = dom F by PARTFUN1:def_2;
hence  x in product F by A14, CARD_3:def_5; ::_thesis: verum
end;
thus  ( ex i being set st
( i in I & B . i = {} & not A . i = {} ) implies ex b1 being set st b1 = {} ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set holds
( ( ( for i being set st i in I & B . i = {} holds
A . i = {} ) & ( for x being set holds
( x in b1 iff x is ManySortedFunction of A,B ) ) & ( for x being set holds
( x in b2 iff x is ManySortedFunction of A,B ) ) implies b1 = b2 ) & ( ex i being set st
( i in I & B . i = {} & not A . i = {} ) & b1 = {} & b2 = {} implies b1 = b2 ) )
proof
let it1, it2 be set ; ::_thesis: ( ( ( for i being set st i in I & B . i = {} holds
A . i = {} ) & ( for x being set holds
( x in it1 iff x is ManySortedFunction of A,B ) ) & ( for x being set holds
( x in it2 iff x is ManySortedFunction of A,B ) ) implies it1 = it2 ) & ( ex i being set st
( i in I & B . i = {} & not A . i = {} ) & it1 = {} & it2 = {} implies it1 = it2 ) )
hereby  ::_thesis: ( ex i being set st
( i in I & B . i = {} & not A . i = {} ) & it1 = {} & it2 = {} implies it1 = it2 )
assume  for i being set st i in I & B . i = {} holds
A . i = {} ; ::_thesis: ( ( for x being set holds
( x in it1 iff x is ManySortedFunction of A,B ) ) & ( for x being set holds
( x in it2 iff x is ManySortedFunction of A,B ) ) implies it1 = it2 )
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 ) ; ::_thesis: it1 = it2
now__::_thesis:_for_x_being_set_holds_
(_x_in_it1_iff_x_in_it2_)
let x be set ; ::_thesis: ( x in it1 iff x in it2 )
 ( x in it1 iff x is ManySortedFunction of A,B ) by A16;
hence  ( x in it1 iff x in it2 ) by A17; ::_thesis: verum
end;
hence  it1 = it2 by TARSKI:1; ::_thesis: verum
end;
thus  ( ex i being set st
( i in I & B . i = {} & not A . i = {} ) & it1 = {} & it2 = {} implies it1 = it2 ) ; ::_thesis: verum
end;
consistency
 for b1 being set holds verum ;
end;

:: deftheorem Def9 defines Funcs FUNCTOR2:def_9_:_
 for I being set
for A, B being ManySortedSet of I
for b4 being set holds
( ( ( for i being set st i in I & B . i = {} holds
A . i = {} ) implies ( b4 = Funcs (A,B) iff for x being set holds
( x in b4 iff x is ManySortedFunction of A,B ) ) ) & ( ex i being set st
( i in I & B . i = {} & not A . i = {} ) implies ( b4 = Funcs (A,B) iff b4 = {} ) ) );

definition
let A, B be non empty transitive with_units AltCatStr ;
func Funct (A,B) ->  set  means :Def10: :: FUNCTOR2:def 10
 for x being set holds
( x in it iff x is strict covariant Functor of A,B );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff x is strict covariant Functor of A,B )
proof
set A9 = Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]);
set sAA =  {  ( the Arrows of B * f) where f is Element of Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]) : verum  }  ;
set f = the Element of Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]);
 the Arrows of B * the Element of Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]) in  {  ( the Arrows of B * f) where f is Element of Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]) : verum  }  ;
then reconsider sAA =  {  ( the Arrows of B * f) where f is Element of Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]) : verum  }  as non empty set ;
defpred S1[ set , set ] means  ex f being Covariant bifunction of the carrier of A, the carrier of B ex m being 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 S2[ set , set ] 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 set st S2[x,y] & S2[x,z] holds
y = z ;
consider XX being set  such that
A2: for x being set holds
( x in XX iff ex y being set st
( y in sAA & S2[y,x] ) ) from TARSKI:sch_1(A1);
A3: for x, y, z being set st S1[x,y] & S1[x,z] holds
y = z
proof
let x, y, z be set ; ::_thesis: ( S1[x,y] & S1[x,z] implies y = z )
given f being Covariant bifunction of the carrier of A, the carrier of B, m being 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 ; ::_thesis: ( not S1[x,z] or y = z )
given f1 being Covariant bifunction of the carrier of A, the carrier of B, m1 being 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 ; ::_thesis: y = z
 f = f1 by A4, A6, XTUPLE_0:1;
hence  y = z by A4, A5, A6, A7, XTUPLE_0:1; ::_thesis: verum
end;
consider X being set  such that
A8: for x being set holds
( x in X iff ex y being set st
( y in [:(Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:])),(union XX):] & S1[y,x] ) ) from TARSKI:sch_1(A3);
take  X ; ::_thesis: for x being set holds
( x in X iff x is strict covariant Functor of A,B )
let x be set ; ::_thesis: ( x in X iff x is strict covariant Functor of A,B )
thus  ( x in X implies x is strict covariant Functor of A,B ) ::_thesis: ( x is strict covariant Functor of A,B implies x in X )
proof
assume  x in X ; ::_thesis: x is strict covariant Functor of A,B
then  ex y being set st
( y in [:(Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:])),(union XX):] & ex f being Covariant bifunction of the carrier of A, the carrier of B ex m being 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  x is strict covariant Functor of A,B ; ::_thesis: verum
end;
assume  x is strict covariant Functor of A,B ; ::_thesis: x in X
then reconsider F = x as strict covariant 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 ;
A9: for o1, o2 being 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; ::_thesis: ( the Arrows of A . (o1,o2) <> {} implies the Arrows of B . (f . (o1,o2)) <> {} )
assume A10: the Arrows of A . (o1,o2) <> {} ; ::_thesis: the Arrows of B . (f . (o1,o2)) <> {}
 the Arrows of A . (o1,o2) = <^o1,o2^> ;
hence  the Arrows of B . (f . (o1,o2)) <> {} by A10, FUNCTOR0:def_11; ::_thesis: verum
end;
A11: for o1, o2 being 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; ::_thesis: ( the Arrows of A . (o1,o2) <> {} implies the Arrows of B . [(F . o1),(F . o2)] <> {} )
assume A12: the Arrows of A . (o1,o2) <> {} ; ::_thesis: the Arrows of B . [(F . o1),(F . o2)] <> {}
 f . (o1,o2) = [(F . o1),(F . o2)] by FUNCTOR0:22;
hence  the Arrows of B . [(F . o1),(F . o2)] <> {} by A9, A12; ::_thesis: verum
end;
 y in [:(Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:])),(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 being set st i in [: the carrier of A, the carrier of A:] & the Arrows of A . i <> {} holds
the Arrows of B . (f . i) <> {}
proof
let i be set ; ::_thesis: ( i in [: the carrier of A, the carrier of A:] & the Arrows of A . i <> {} implies the Arrows of B . (f . i) <> {} )
assume that
A14: i in [: the carrier of A, the carrier of A:] and
A15: the Arrows of A . i <> {} ; ::_thesis: the Arrows of B . (f . i) <> {}
consider o1, o2 being set  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  the Arrows of B . (f . i) <> {} by A11, A18; ::_thesis: verum
end;
 for i being set st i in [: the carrier of A, the carrier of A:] & the Arrows of A . i <> {} holds
AA . i <> {}
proof
let i be set ; ::_thesis: ( i in [: the carrier of A, the carrier of A:] & the Arrows of A . i <> {} implies AA . i <> {} )
assume A19: i in [: the carrier of A, the carrier of A:] ; ::_thesis: ( not the Arrows of A . i <> {} or AA . i <> {} )
assume A20: the Arrows of A . i <> {} ; ::_thesis: AA . i <> {}
 AA . i = the Arrows of B . (f . i) by A19, FUNCT_2:15;
hence  AA . i <> {} by A13, A19, A20; ::_thesis: verum
end;
then  ( m is ManySortedFunction of the Arrows of A,AA & ( for i being set st i in [: the carrier of A, the carrier of A:] & AA . i = {} holds
the Arrows of A . i = {} ) ) by FUNCTOR0:def_4;
then A21: m in Funcs ( the Arrows of A,AA) by Def9;
A22: f in Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]) 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  y in [:(Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:])),(union XX):] by A22, ZFMISC_1:def_2; ::_thesis: verum
end;
hence  x in X by A8; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff x is strict covariant Functor of A,B ) ) & ( for x being set holds
( x in b2 iff x is strict covariant Functor of A,B ) ) holds
b1 = b2
proof
let it1, it2 be set ; ::_thesis: ( ( for x being set holds
( x in it1 iff x is strict covariant Functor of A,B ) ) & ( for x being set holds
( x in it2 iff x is strict covariant Functor of A,B ) ) implies it1 = it2 )
assume that
A23: for x being set holds
( x in it1 iff x is strict covariant Functor of A,B ) and
A24: for x being set holds
( x in it2 iff x is strict covariant Functor of A,B ) ; ::_thesis: it1 = it2
now__::_thesis:_for_x_being_set_holds_
(_x_in_it1_iff_x_in_it2_)
let x be set ; ::_thesis: ( x in it1 iff x in it2 )
 ( x in it1 iff x is strict covariant Functor of A,B ) by A23;
hence  ( x in it1 iff x in it2 ) by A24; ::_thesis: verum
end;
hence  it1 = it2 by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def10 defines Funct FUNCTOR2:def_10_:_
 for A, B being non empty transitive with_units AltCatStr
for b3 being set holds
( b3 = Funct (A,B) iff for x being set holds
( x in b3 iff x is strict covariant Functor of A,B ) );

definition
let A, B be category;
func Functors (A,B) ->  non empty transitive strict AltCatStr  means :: FUNCTOR2:def 11
( the carrier of it = Funct (A,B) & ( for F, G being strict covariant Functor of A,B
for 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 holds
for t1 being natural_transformation of F,G
for 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
 ex b1 being non empty transitive strict AltCatStr st
( the carrier of b1 = Funct (A,B) & ( for F, G being strict covariant Functor of A,B
for x being set holds
( x in the Arrows of b1 . (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 holds
for t1 being natural_transformation of F,G
for t2 being natural_transformation of G,H ex f being Function st
( f = the Comp of b1 . (F,G,H) & f . (t2,t1) = t2 `*` t1 ) ) )
proof
defpred S1[ set , set , set ] means  for f, g, h being strict covariant Functor of A,B st [f,g,h] = $3 holds
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 S2[ set , set ] means  for f, g being strict covariant Functor of A,B st [f,g] = $1 holds
for x being set holds
( x in $2 iff ( f is_naturally_transformable_to g & x is natural_transformation of f,g ) );
A1: for i being set st i in [:(Funct (A,B)),(Funct (A,B)):] holds
ex j being set st S2[i,j]
proof
let i be set ; ::_thesis: ( i in [:(Funct (A,B)),(Funct (A,B)):] implies ex j being set st S2[i,j] )
assume  i in [:(Funct (A,B)),(Funct (A,B)):] ; ::_thesis: ex j being set st S2[i,j]
then consider f, g being set  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 = f, g = g as strict covariant Functor of A,B by A2, Def10;
defpred S3[ object of A, set ] means $2 = <^(f . $1),(g . $1)^>;
defpred S4[ set ] means ( f is_naturally_transformable_to g & $1 is natural_transformation of f,g );
A4: for a being Element of A ex j being set st S3[a,j] ;
consider N being ManySortedSet of the carrier of A such that
A5: for a being Element of A holds S3[a,N . a] from PBOOLE:sch_6(A4);
consider j being set  such that
A6: for x being set holds
( x in j iff ( x in product N & S4[x] ) ) from XBOOLE_0:sch_1();
take  j ; ::_thesis: S2[i,j]
let f9, g9 be strict covariant Functor of A,B; ::_thesis: ( [f9,g9] = i implies for x being set holds
( x in j iff ( f9 is_naturally_transformable_to g9 & x is natural_transformation of f9,g9 ) ) )
assume A7: [f9,g9] = i ; ::_thesis: for x being set holds
( x in j iff ( f9 is_naturally_transformable_to g9 & x is natural_transformation of f9,g9 ) )
let x be set ; ::_thesis: ( x in j iff ( f9 is_naturally_transformable_to g9 & x is natural_transformation of f9,g9 ) )
thus  ( x in j implies ( f9 is_naturally_transformable_to g9 & x is natural_transformation of f9,g9 ) ) ::_thesis: ( f9 is_naturally_transformable_to g9 & x is natural_transformation of f9,g9 implies x in j )
proof
assume A8: x in j ; ::_thesis: ( f9 is_naturally_transformable_to g9 & x is natural_transformation of f9,g9 )
 ( f9 = f & g9 = g ) by A3, A7, XTUPLE_0:1;
hence  ( f9 is_naturally_transformable_to g9 & x is natural_transformation of f9,g9 ) by A6, A8; ::_thesis: verum
end;
thus  ( f9 is_naturally_transformable_to g9 & x is natural_transformation of f9,g9 implies x in j ) ::_thesis: verum
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 ; ::_thesis: x in j
reconsider h = x as ManySortedSet of the carrier of A by A11;
A12: f9 is_transformable_to g9 by A10, Def6;
A13: for i9 being set st i9 in the carrier of A holds
h . i9 in N . i9
proof
let i9 be set ; ::_thesis: ( i9 in the carrier of A implies h . i9 in N . i9 )
assume  i9 in the carrier of A ; ::_thesis: h . i9 in N . i9
then reconsider i9 = i9 as Element of A ;
A14: S3[i9,N . i9] by A5;
 ( <^(f . i9),(g . i9)^> <> {} & h . i9 is Element of <^(f . i9),(g . i9)^> ) by A11, A12, A9, Def1, Def2;
hence  h . i9 in N . i9 by A14; ::_thesis: verum
end;
A15: for i9 being set st i9 in dom N holds
h . i9 in N . i9
proof
A16: dom N = the carrier of A by PARTFUN1:def_2;
let i9 be set ; ::_thesis: ( i9 in dom N implies h . i9 in N . i9 )
assume  i9 in dom N ; ::_thesis: h . i9 in N . i9
hence  h . i9 in N . i9 by A13, A16; ::_thesis: verum
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  x in j by A6, A10, A11, A9; ::_thesis: verum
end;
end;
consider a being ManySortedSet of [:(Funct (A,B)),(Funct (A,B)):] such that
A17: for i being set st i in [:(Funct (A,B)),(Funct (A,B)):] holds
S2[i,a . i] from PBOOLE:sch_3(A1);
A18: for o being set st o in [:(Funct (A,B)),(Funct (A,B)),(Funct (A,B)):] holds
for x being set st x in {|a,a|} . o holds
ex y being set st
( y in {|a|} . o & S1[y,x,o] )
proof
let o be set ; ::_thesis: ( o in [:(Funct (A,B)),(Funct (A,B)),(Funct (A,B)):] implies for x being set st x in {|a,a|} . o holds
ex y being set st
( y in {|a|} . o & S1[y,x,o] ) )
assume  o in [:(Funct (A,B)),(Funct (A,B)),(Funct (A,B)):] ; ::_thesis: for x being set st x in {|a,a|} . o holds
ex y being set st
( y in {|a|} . o & S1[y,x,o] )
then  o in [:[:(Funct (A,B)),(Funct (A,B)):],(Funct (A,B)):] by ZFMISC_1:def_3;
then consider ff, h being set  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 being set  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 being set st x in {|a,a|} . o holds
ex y being set st
( y in {|a|} . o & S1[y,x,o] )
proof
reconsider i9 = i, j9 = j, k9 = k as strict covariant Functor of A,B by Def10;
let x be set ; ::_thesis: ( x in {|a,a|} . o implies ex y being set st
( y in {|a|} . o & S1[y,x,o] ) )
A27: [i9,k9] in [:(Funct (A,B)),(Funct (A,B)):] by ZFMISC_1:def_2;
assume  x in {|a,a|} . o ; ::_thesis: ex y being set st
( y in {|a|} . o & S1[y,x,o] )
then consider x2, x1 being set  such that
A28: x2 in a . (j,k) and
A29: x1 in a . (i,j) and
A30: x = [x2,x1] by A24, A26, ZFMISC_1:def_2;
A31: x2 in a . [j,k] by A28;
then A32: j9 is_naturally_transformable_to k9 by A17;
reconsider x2 = x2 as natural_transformation of j9,k9 by A17, A31;
A33: x1 in a . [i,j] by A29;
then reconsider x1 = x1 as natural_transformation of i9,j9 by A17;
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 holds
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; ::_thesis: ( [f,g,h] = o implies 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 )
assume A35: [f,g,h] = o ; ::_thesis: 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
A36: j9 = g by A24, A35, XTUPLE_0:3;
then reconsider x2 = 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; ::_thesis: for t2 being natural_transformation of g,h st [t2,t1] = x & ex v being Function st v . x = vv holds
vv = t2 `*` t1
let t2 be natural_transformation of g,h; ::_thesis: ( [t2,t1] = x & ex v being Function st v . x = vv implies vv = t2 `*` t1 )
assume that
A38: [t2,t1] = x and
 ex v being Function st v . x = vv ; ::_thesis: vv = t2 `*` t1
 x2 = t2 by A30, A38, XTUPLE_0:1;
hence  vv = t2 `*` t1 by A30, A38, A36, A37, XTUPLE_0:1; ::_thesis: verum
end;
 i9 is_naturally_transformable_to j9 by A17, A33;
then  i9 is_naturally_transformable_to k9 by A32, Th8;
then  vv in a . [i9,k9] by A17, A27;
hence  ex y being set st
( y in {|a|} . o & S1[y,x,o] ) by A24, A25, A34; ::_thesis: verum
end;
hence  for x being set st x in {|a,a|} . o holds
ex y being set st
( y in {|a|} . o & S1[y,x,o] ) ; ::_thesis: verum
end;
consider c being ManySortedFunction of {|a,a|},{|a|} such that
A39: for i being set st i in [:(Funct (A,B)),(Funct (A,B)),(Funct (A,B)):] holds
ex v being Function of ({|a,a|} . i),({|a|} . i) st
( v = c . i & ( for x being set st x in {|a,a|} . i holds
S1[v . x,x,i] ) ) from MSSUBFAM:sch_1(A18);
set F = AltCatStr(# (Funct (A,B)),a,c #);
A40: not Funct (A,B) is empty
proof
set f = the strict covariant Functor of A,B;
 the strict covariant Functor of A,B in Funct (A,B) by Def10;
hence  not Funct (A,B) is empty ; ::_thesis: verum
end;
 AltCatStr(# (Funct (A,B)),a,c #) is transitive
proof
let o1, o2, o3 be object of AltCatStr(# (Funct (A,B)),a,c #); :: according to ALTCAT_1:def_2 ::_thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or not <^o1,o3^> = {} )
reconsider a1 = o1, a2 = o2, a3 = o3 as strict covariant Functor of A,B by A40, Def10;
assume that
A41: <^o1,o2^> <> {} and
A42: <^o2,o3^> <> {} ; ::_thesis: not <^o1,o3^> = {}
consider x being set  such that
A43: x in a . [o2,o3] by A42, XBOOLE_0:def_1;
A44: [o2,o3] in [:(Funct (A,B)),(Funct (A,B)):] by A40, ZFMISC_1:def_2;
then A45: a2 is_naturally_transformable_to a3 by A17, A43;
reconsider x = x as natural_transformation of a2,a3 by A17, A44, A43;
consider y being set  such that
A46: y in a . [o1,o2] by A41, XBOOLE_0:def_1;
A47: [o1,o2] in [:(Funct (A,B)),(Funct (A,B)):] by A40, ZFMISC_1:def_2;
then reconsider y = y as natural_transformation of a1,a2 by A17, A46;
 a1 is_naturally_transformable_to a2 by A17, A47, A46;
then A48: a1 is_naturally_transformable_to a3 by A45, Th8;
 ( x `*` y is natural_transformation of a1,a3 & [o1,o3] in [:(Funct (A,B)),(Funct (A,B)):] ) by A40, ZFMISC_1:def_2;
hence  not <^o1,o3^> = {} by A17, A48; ::_thesis: verum
end;
then reconsider F = AltCatStr(# (Funct (A,B)),a,c #) as non empty transitive strict AltCatStr by A40;
take  F ; ::_thesis: ( the carrier of F = Funct (A,B) & ( for F, G being strict covariant Functor of A,B
for 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 ) ) ) & ( for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G & G is_naturally_transformable_to H holds
for t1 being natural_transformation of F,G
for t2 being natural_transformation of G,H ex f being Function st
( f = the Comp of F . (F,G,H) & f . (t2,t1) = t2 `*` t1 ) ) )
thus  the carrier of F = Funct (A,B) ; ::_thesis: ( ( for F, G being strict covariant Functor of A,B
for 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 ) ) ) & ( for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G & G is_naturally_transformable_to H holds
for t1 being natural_transformation of F,G
for t2 being natural_transformation of G,H ex f being Function st
( f = the Comp of F . (F,G,H) & f . (t2,t1) = t2 `*` t1 ) ) )
thus  for f, g being strict covariant Functor of A,B
for 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 ) ) ::_thesis: for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G & G is_naturally_transformable_to H holds
for t1 being natural_transformation of F,G
for t2 being natural_transformation of G,H ex f being Function st
( f = the Comp of F . (F,G,H) & f . (t2,t1) = t2 `*` t1 )
proof
let f, g be strict covariant Functor of A,B; ::_thesis: for 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 ) )
let x be set ; ::_thesis: ( x in the Arrows of F . (f,g) iff ( f is_naturally_transformable_to g & x is natural_transformation of f,g ) )
thus  ( x in the Arrows of F . (f,g) implies ( f is_naturally_transformable_to g & x is natural_transformation of f,g ) ) ::_thesis: ( 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 A49: [f,g] in [:(Funct (A,B)),(Funct (A,B)):] by ZFMISC_1:def_2;
assume  x in the Arrows of F . (f,g) ; ::_thesis: ( f is_naturally_transformable_to g & x is natural_transformation of f,g )
hence  ( f is_naturally_transformable_to g & x is natural_transformation of f,g ) by A17, A49; ::_thesis: verum
end;
thus  ( f is_naturally_transformable_to g & x is natural_transformation of f,g implies x in the Arrows of F . (f,g) ) ::_thesis: verum
proof
 ( f in Funct (A,B) & g in Funct (A,B) ) by Def10;
then A50: [f,g] in [:(Funct (A,B)),(Funct (A,B)):] by ZFMISC_1:87;
assume  ( f is_naturally_transformable_to g & x is natural_transformation of f,g ) ; ::_thesis: x in the Arrows of F . (f,g)
hence  x in the Arrows of F . (f,g) by A17, A50; ::_thesis: verum
end;
end;
let f, g, h be strict covariant Functor of A,B; ::_thesis: ( f is_naturally_transformable_to g & g is_naturally_transformable_to h implies for t1 being natural_transformation of f,g
for t2 being natural_transformation of g,h ex f being Function st
( f = the Comp of F . (f,g,h) & f . (t2,t1) = t2 `*` t1 ) )
assume that
A51: f is_naturally_transformable_to g and
A52: g is_naturally_transformable_to h ; ::_thesis: for t1 being natural_transformation of f,g
for t2 being natural_transformation of g,h ex f being Function st
( f = the Comp of F . (f,g,h) & f . (t2,t1) = t2 `*` t1 )
let t1 be natural_transformation of f,g; ::_thesis: for t2 being natural_transformation of g,h ex f being Function st
( f = the Comp of F . (f,g,h) & f . (t2,t1) = t2 `*` t1 )
let t2 be natural_transformation of g,h; ::_thesis: ex f being Function st
( f = the Comp of F . (f,g,h) & f . (t2,t1) = t2 `*` t1 )
A53: f in Funct (A,B) by Def10;
then reconsider T = Funct (A,B) as non empty set ;
A54: g in Funct (A,B) by Def10;
then A55: [f,g] in [:(Funct (A,B)),(Funct (A,B)):] by A53, ZFMISC_1:87;
A56: h in Funct (A,B) by Def10;
then  [g,h] in [:(Funct (A,B)),(Funct (A,B)):] by A54, ZFMISC_1:87;
then A57: t2 in a . [g,h] by A17, A52;
reconsider i = f, j = g, k = h as Element of T by Def10;
A58: {|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 A56, A55, ZFMISC_1:87;
then consider v being Function of ({|a,a|} . [f,g,h]),({|a|} . [f,g,h]) such that
A59: v = c . [f,g,h] and
A60: for x being set st x in {|a,a|} . [f,g,h] holds
S1[v . x,x,[f,g,h]] by A39;
 t1 in a . [f,g] by A17, A51, A55;
then  [t2,t1] in {|a,a|} . [f,g,h] by A58, A57, ZFMISC_1:87;
then A61: v . (t2,t1) = t2 `*` t1 by A60;
 v = c . (f,g,h) by A59, MULTOP_1:def_1;
hence  ex f being Function st
( f = the Comp of F . (f,g,h) & f . (t2,t1) = t2 `*` t1 ) by A61; ::_thesis: verum
end;
uniqueness
 for b1, b2 being non empty transitive strict AltCatStr st the carrier of b1 = Funct (A,B) & ( for F, G being strict covariant Functor of A,B
for x being set holds
( x in the Arrows of b1 . (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 holds
for t1 being natural_transformation of F,G
for t2 being natural_transformation of G,H ex f being Function st
( f = the Comp of b1 . (F,G,H) & f . (t2,t1) = t2 `*` t1 ) ) & the carrier of b2 = Funct (A,B) & ( for F, G being strict covariant Functor of A,B
for x being set holds
( x in the Arrows of b2 . (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 holds
for t1 being natural_transformation of F,G
for t2 being natural_transformation of G,H ex f being Function st
( f = the Comp of b2 . (F,G,H) & f . (t2,t1) = t2 `*` t1 ) ) holds
b1 = b2
proof
let C1, C2 be non empty transitive strict AltCatStr ; ::_thesis: ( the carrier of C1 = Funct (A,B) & ( for F, G being strict covariant Functor of A,B
for 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 ) ) ) & ( for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G & G is_naturally_transformable_to H holds
for t1 being natural_transformation of F,G
for 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 ) ) & the carrier of C2 = Funct (A,B) & ( for F, G being strict covariant Functor of A,B
for 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 ) ) ) & ( for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G & G is_naturally_transformable_to H holds
for t1 being natural_transformation of F,G
for 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 ) ) implies C1 = C2 )
assume that
A62: the carrier of C1 = Funct (A,B) and
A63: for F, G being strict covariant Functor of A,B
for 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
A64: for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G & G is_naturally_transformable_to H holds
for t1 being natural_transformation of F,G
for 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
A65: the carrier of C2 = Funct (A,B) and
A66: for F, G being strict covariant Functor of A,B
for 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
A67: for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G & G is_naturally_transformable_to H holds
for t1 being natural_transformation of F,G
for 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 ) ; ::_thesis: C1 = C2
set R = the carrier of C1;
set T = the carrier of C2;
set N = the Arrows of C1;
set M = the Arrows of C2;
set O = the Comp of C1;
set P = the Comp of C2;
A68: for i, j being set st i in the carrier of C1 & j in the carrier of C2 holds
the Arrows of C1 . (i,j) = the Arrows of C2 . (i,j)
proof
let i, j be set ; ::_thesis: ( i in the carrier of C1 & j in the carrier of C2 implies the Arrows of C1 . (i,j) = the Arrows of C2 . (i,j) )
assume that
A69: i in the carrier of C1 and
A70: j in the carrier of C2 ; ::_thesis: the Arrows of C1 . (i,j) = the Arrows of C2 . (i,j)
reconsider g = j as strict covariant Functor of A,B by A65, A70, Def10;
reconsider f = i as strict covariant Functor of A,B by A62, A69, Def10;
now__::_thesis:_for_x_being_set_holds_
(_x_in_the_Arrows_of_C1_._(i,j)_iff_x_in_the_Arrows_of_C2_._(i,j)_)
let x be set ; ::_thesis: ( x in the Arrows of C1 . (i,j) iff x in the Arrows of C2 . (i,j) )
 ( x in the Arrows of C1 . (i,j) iff ( f is_naturally_transformable_to g & x is natural_transformation of f,g ) ) by A63;
hence  ( x in the Arrows of C1 . (i,j) iff x in the Arrows of C2 . (i,j) ) by A66; ::_thesis: verum
end;
hence  the Arrows of C1 . (i,j) = the Arrows of C2 . (i,j) by TARSKI:1; ::_thesis: verum
end;
then A71: the Arrows of C1 = the Arrows of C2 by A62, A65, ALTCAT_1:6;
 for i, j, k being set st i in the carrier of C1 & j in the carrier of C1 & k in the carrier of C1 holds
the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k)
proof
let i, j, k be set ; ::_thesis: ( i in the carrier of C1 & j in the carrier of C1 & k in the carrier of C1 implies the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k) )
assume that
A72: i in the carrier of C1 and
A73: j in the carrier of C1 and
A74: k in the carrier of C1 ; ::_thesis: the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k)
reconsider h = k as strict covariant Functor of A,B by A62, A74, Def10;
reconsider g = j as strict covariant Functor of A,B by A62, A73, Def10;
reconsider f = i as strict covariant Functor of A,B by A62, A72, Def10;
percases ( the Arrows of C1 . (i,j) = {} or the Arrows of C1 . (j,k) = {} or ( the Arrows of C1 . (i,j) <> {} & the Arrows of C1 . (j,k) <> {} ) ) ;
supposeA75: ( the Arrows of C1 . (i,j) = {} or the Arrows of C1 . (j,k) = {} ) ; ::_thesis: the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k)
thus  the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k) ::_thesis: verum
proof
percases ( the Arrows of C1 . (i,j) = {} or the Arrows of C1 . (j,k) = {} ) by A75;
supposeA76: the Arrows of C1 . (i,j) = {} ; ::_thesis: the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k)
reconsider T = the carrier of C2 as non empty set ;
reconsider i9 = i, j9 = j, k9 = k as Element of T by A62, A65, A72, A73, A74;
 the Arrows of C2 . (i,j) = {} by A62, A65, A68, A76, ALTCAT_1:6;
then A77: [:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):] = {} by ZFMISC_1:90;
A78: {| the Arrows of C2, the Arrows of C2|} . [i9,j9,k9] = {| the Arrows of C2, the Arrows of C2|} . (i9,j9,k9) by MULTOP_1:def_1
.= [:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):] by ALTCAT_1:def_4 ;
A79: {| the Arrows of C2|} . [i9,j9,k9] = {| the Arrows of C2|} . (i9,j9,k9) by MULTOP_1:def_1
.= the Arrows of C2 . (i9,k9) by ALTCAT_1:def_3 ;
 the Comp of C2 . [i9,j9,k9] = the Comp of C2 . (i9,j9,k9) by MULTOP_1:def_1;
then A80: the Comp of C2 . (i9,j9,k9) is Function of [:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):],( the Arrows of C2 . (i9,k9)) by A78, A79, PBOOLE:def_15;
A81: {| the Arrows of C2, the Arrows of C2|} . [i9,j9,k9] = {| the Arrows of C2, the Arrows of C2|} . (i9,j9,k9) by MULTOP_1:def_1
.= [:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):] by ALTCAT_1:def_4 ;
A82: {| the Arrows of C2|} . [i9,j9,k9] = {| the Arrows of C2|} . (i9,j9,k9) by MULTOP_1:def_1
.= the Arrows of C2 . (i9,k9) by ALTCAT_1:def_3 ;
 the Comp of C1 . [i9,j9,k9] = the Comp of C1 . (i9,j9,k9) by MULTOP_1:def_1;
then  the Comp of C1 . (i9,j9,k9) is Function of [:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):],( the Arrows of C2 . (i9,k9)) by A62, A65, A71, A81, A82, PBOOLE:def_15;
hence  the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k) by A77, A80; ::_thesis: verum
end;
supposeA83: the Arrows of C1 . (j,k) = {} ; ::_thesis: the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k)
reconsider T = the carrier of C2 as non empty set ;
reconsider i9 = i, j9 = j, k9 = k as Element of T by A62, A65, A72, A73, A74;
 the Arrows of C2 . (j,k) = {} by A62, A65, A68, A83, ALTCAT_1:6;
then A84: [:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):] = {} by ZFMISC_1:90;
A85: {| the Arrows of C2, the Arrows of C2|} . [i9,j9,k9] = {| the Arrows of C2, the Arrows of C2|} . (i9,j9,k9) by MULTOP_1:def_1
.= [:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):] by ALTCAT_1:def_4 ;
A86: {| the Arrows of C2|} . [i9,j9,k9] = {| the Arrows of C2|} . (i9,j9,k9) by MULTOP_1:def_1
.= the Arrows of C2 . (i9,k9) by ALTCAT_1:def_3 ;
 the Comp of C2 . [i9,j9,k9] = the Comp of C2 . (i9,j9,k9) by MULTOP_1:def_1;
then A87: the Comp of C2 . (i9,j9,k9) is Function of [:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):],( the Arrows of C2 . (i9,k9)) by A85, A86, PBOOLE:def_15;
A88: {| the Arrows of C2, the Arrows of C2|} . [i9,j9,k9] = {| the Arrows of C2, the Arrows of C2|} . (i9,j9,k9) by MULTOP_1:def_1
.= [:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):] by ALTCAT_1:def_4 ;
A89: {| the Arrows of C2|} . [i9,j9,k9] = {| the Arrows of C2|} . (i9,j9,k9) by MULTOP_1:def_1
.= the Arrows of C2 . (i9,k9) by ALTCAT_1:def_3 ;
 the Comp of C1 . [i9,j9,k9] = the Comp of C1 . (i9,j9,k9) by MULTOP_1:def_1;
then  the Comp of C1 . (i9,j9,k9) is Function of [:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):],( the Arrows of C2 . (i9,k9)) by A62, A65, A71, A88, A89, PBOOLE:def_15;
hence  the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k) by A84, A87; ::_thesis: verum
end;
end;
end;
end;
supposethat A90: the Arrows of C1 . (i,j) <> {} and
A91: the Arrows of C1 . (j,k) <> {} ; ::_thesis: the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k)
reconsider T = the carrier of C2 as non empty set ;
reconsider i9 = i, j9 = j, k9 = k as Element of T by A62, A65, A72, A73, A74;
A92: {| the Arrows of C2, the Arrows of C2|} . [i9,j9,k9] = {| the Arrows of C2, the Arrows of C2|} . (i9,j9,k9) by MULTOP_1:def_1
.= [:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):] by ALTCAT_1:def_4 ;
A93: {| the Arrows of C2|} . [i9,j9,k9] = {| the Arrows of C2|} . (i9,j9,k9) by MULTOP_1:def_1
.= the Arrows of C2 . (i9,k9) by ALTCAT_1:def_3 ;
 the Comp of C2 . [i9,j9,k9] = the Comp of C2 . (i9,j9,k9) by MULTOP_1:def_1;
then reconsider t2 = the Comp of C2 . (i,j,k) as Function of [:( the Arrows of C2 . (j,k)),( the Arrows of C2 . (i,j)):],( the Arrows of C2 . (i,k)) by A92, A93, PBOOLE:def_15;
A94: {| the Arrows of C2, the Arrows of C2|} . [i9,j9,k9] = {| the Arrows of C2, the Arrows of C2|} . (i9,j9,k9) by MULTOP_1:def_1
.= [:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):] by ALTCAT_1:def_4 ;
A95: {| the Arrows of C2|} . [i9,j9,k9] = {| the Arrows of C2|} . (i9,j9,k9) by MULTOP_1:def_1
.= the Arrows of C2 . (i9,k9) by ALTCAT_1:def_3 ;
 the Comp of C1 . [i9,j9,k9] = the Comp of C1 . (i9,j9,k9) by MULTOP_1:def_1;
then reconsider t1 = the Comp of C1 . (i,j,k) as Function of [:( the Arrows of C2 . (j,k)),( the Arrows of C2 . (i,j)):],( the Arrows of C2 . (i,k)) by A62, A65, A71, A94, A95, PBOOLE:def_15;
A96: the Arrows of C2 . (j,k) <> {} by A62, A65, A68, A91, ALTCAT_1:6;
A97: the Arrows of C2 . (i,j) <> {} by A62, A65, A68, A90, ALTCAT_1:6;
 for a being Element of the Arrows of C2 . (j,k)
for b being Element of the Arrows of C2 . (i,j) holds t1 . (a,b) = t2 . (a,b)
proof
let a be Element of the Arrows of C2 . (j,k); ::_thesis: for b being Element of the Arrows of C2 . (i,j) holds t1 . (a,b) = t2 . (a,b)
let b be Element of the Arrows of C2 . (i,j); ::_thesis: t1 . (a,b) = t2 . (a,b)
 a in the Arrows of C2 . (j,k) by A96;
then A98: g is_naturally_transformable_to h by A66;
reconsider a = a as natural_transformation of g,h by A66, A96;
 b in the Arrows of C2 . (i,j) by A97;
then A99: f is_naturally_transformable_to g by A66;
reconsider b = b as natural_transformation of f,g by A66, A97;
 ( ex t19 being Function st
( t19 = the Comp of C1 . (f,g,h) & t19 . (a,b) = a `*` b ) & ex t29 being Function st
( t29 = the Comp of C2 . (f,g,h) & t29 . (a,b) = a `*` b ) ) by A64, A67, A98, A99;
hence  t1 . (a,b) = t2 . (a,b) ; ::_thesis: verum
end;
hence  the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k) by BINOP_1:2; ::_thesis: verum
end;
end;
end;
hence  C1 = C2 by A62, A65, A71, ALTCAT_1:8; ::_thesis: verum
end;
end;

:: deftheorem  defines Functors FUNCTOR2:def_11_:_
 for A, B being category
for b3 being non empty transitive strict AltCatStr holds
( b3 = Functors (A,B) iff ( the carrier of b3 = Funct (A,B) & ( for F, G being strict covariant Functor of A,B
for x being set holds
( x in the Arrows of b3 . (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 holds
for t1 being natural_transformation of F,G
for t2 being natural_transformation of G,H ex f being Function st
( f = the Comp of b3 . (F,G,H) & f . (t2,t1) = t2 `*` t1 ) ) ) );