:: Category of Functors between Alternative Categories
:: by Robert Nieszczerzewski
::
:: Received June 12, 1997
:: Copyright (c) 1997-2026 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; :: redefines idt (FUNCTOR2, definition)
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;