Copyright (c) 1997 Association of Mizar Users
environ
vocabulary RELAT_2, ALTCAT_1, MSUALG_6, FUNCTOR0, CAT_1, FUNCT_1, BOOLE,
NATTRA_1, PBOOLE, QC_LANG1, FUNCT_2, PRALG_1, CARD_3, RELAT_1, CAT_2,
TARSKI, FUNCTOR2;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCTOR0, MCART_1, DOMAIN_1,
RELAT_1, STRUCT_0, CARD_3, FUNCT_1, FUNCT_2, BINOP_1, MULTOP_1, FRAENKEL,
PBOOLE, MSUALG_1, ALTCAT_1;
constructors FUNCTOR0, DOMAIN_1;
clusters STRUCT_0, ALTCAT_1, FUNCTOR0, RELSET_1, SUBSET_1, XBOOLE_0;
requirements SUBSET, BOOLE;
definitions ALTCAT_1;
theorems MCART_1, MULTOP_1, FUNCT_2, ZFMISC_1, ALTCAT_1, PBOOLE, BINOP_1,
TARSKI, ALTCAT_2, STRUCT_0, FUNCTOR0, MSUALG_1, CARD_3, XBOOLE_0,
PARTFUN1;
schemes TARSKI, MSUALG_9, MSUALG_1, MSSUBFAM, XBOOLE_0;
begin
definition let A be transitive with_units (non empty AltCatStr),
B be with_units (non empty AltCatStr);
cluster -> feasible id-preserving Functor of A, B;
coherence by FUNCTOR0:def 26;
end;
definition let A be transitive with_units (non empty AltCatStr),
B be with_units (non empty AltCatStr);
cluster covariant -> Covariant comp-preserving Functor of A, B;
coherence by FUNCTOR0:def 27;
cluster Covariant comp-preserving -> covariant Functor of A, B;
coherence by FUNCTOR0:def 27;
cluster contravariant -> Contravariant comp-reversing Functor of A, B;
coherence by FUNCTOR0:def 28;
cluster Contravariant comp-reversing -> contravariant Functor of A, B;
coherence by FUNCTOR0:def 28;
end;
canceled;
theorem Th2:
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;
A1: <^a,a^> <> {} by ALTCAT_2:def 7;
<^F.a,F.a^> <> {} by ALTCAT_2:def 7;
hence F.idm a = Morph-Map(F,a,a).idm a by A1,FUNCTOR0:def 16
.= idm (F.a) by FUNCTOR0:def 21;
end;
begin :: Transformations
definition
let A,B be transitive with_units (non empty AltCatStr),
F1,F2 be covariant Functor of A,B;
pred F1 is_transformable_to F2 means
:Def1: for a being object of A holds <^F1.a,F2.a^> <> {};
reflexivity by ALTCAT_2:def 7;
end;
canceled;
theorem Th4:
for A,B being transitive with_units (non empty AltCatStr),
F,F1,F2 being covariant 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 covariant 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,Def1;
hence thesis by ALTCAT_1:def 4;
end;
definition
let A,B be transitive with_units (non empty AltCatStr),
F1,F2 be covariant 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[set,set] means
ex o being object of A st $1 = o & $2 in <^F1.o,F2.o^>;
A2: for a being Element of A ex j being set st P[a,j]
proof
let a be Element of A;
reconsider
o = a as object of A;
<^F1.o,F2.o^> <> {} by A1,Def1;
then consider j be set such that
A3: j in <^F1.o,F2.o^> by XBOOLE_0:def 1;
thus thesis by A3;
end;
consider t being ManySortedSet of the carrier of A such that
A4: for a being Element of A holds P[a,t.a]
from MSSExD(A2);
take t;
let a be object of A;
ex o being object of A st a = o & t.a in <^F1.o,F2.o^> by A4;
hence thesis;
end;
end;
definition
let A,B be transitive with_units (non empty AltCatStr);
let F be covariant 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[set,set] means
ex o being object of A st $1 = o & $2 = idm (F.o);
A1: for a being Element of A
ex j being set st P[a,j]
proof
let a be Element of A;
reconsider
o = a as object of A;
consider j be set such that
A2: j = idm (F.o);
thus thesis by A2;
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 MSSExD(A1);
for a be object of A holds t.a is Morphism of F.a,F.a
proof
let o be Element of A;
consider
a being object of A such that
A4: o = a & t.o = idm (F.a) by A3;
thus thesis by A4;
end;
then reconsider t as transformation of F,F by Def2;
take t;
let a be Element of A;
consider
o being object of A such that
A5: a = o & t.a = idm (F.o) by A3;
thus thesis by A5;
end;
uniqueness
proof
let it1,it2 be transformation of F,F such that
A6: for a being object of A holds it1.a = idm (F.a) and
A7: for a being object of A holds it2.a = idm (F.a);
now
let a be set;
assume a in the carrier of A;
then reconsider o = a as object of A;
thus it1.a = idm (F.o) by A6
.= it2.a by A7;
end;
hence it1 = it2 by PBOOLE:3;
end;
end;
definition
let A,B be transitive with_units (non empty AltCatStr),
F1,F2 be covariant 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 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;
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[set,set] means
ex o being object of A st $1 = o & $2 = (t2!o) * (t1!o);
A3: for a being Element of A
ex j being set st P[a,j]
proof
let a be Element of A;
reconsider o = a as object of A;
consider j be set such that
A4: j = (t2!o) * (t1!o);
thus thesis by A4;
end;
consider t being ManySortedSet of the carrier of A such that
A5: for a being Element of A holds P[a,t.a]
from MSSExD(A3);
A6: F is_transformable_to F2 by A1,A2,Th4;
for a be object of A holds t.a is Morphism of F.a,F2.a
proof
let o be Element of A;
consider
a being object of A such that
A7: o = a & t.o = (t2!a) * (t1!a) by A5;
thus thesis by A7;
end;
then reconsider
t' = t as transformation of F,F2 by A6,Def2;
take t';
let a be Element of A;
consider o being object of A such that
A8: a = o & t.a = (t2!o) * (t1!o) by A5;
thus thesis by A6,A8,Def4;
end;
uniqueness
proof
let it1,it2 be transformation of F,F2 such that
A9: for a being object of A holds it1!a = (t2!a)*(t1!a) and
A10: for a being object of A holds it2!a = (t2!a)*(t1!a);
A11: F is_transformable_to F2 by A1,A2,Th4;
now
let a be set;
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 A11,Def4
.= (t2!o)*(t1!o) by A9
.= it2!o by A10
.= (it2 qua ManySortedSet of the carrier of A).a by A11,Def4;
end;
hence it1 = it2 by PBOOLE:3;
end;
end;
theorem Th5:
for A,B being transitive with_units (non empty AltCatStr),
F1,F2 being covariant 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 covariant 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 set;
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 t1 = t2 by PBOOLE:3;
end;
theorem Th6:
for A,B being transitive with_units (non empty AltCatStr),
F being covariant 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 covariant 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 Th7:
for A,B being transitive with_units (non empty AltCatStr),
F1,F2 being covariant 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 covariant 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^> <> {} & <^F2.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 Th6
.= t!a by A2,ALTCAT_1:24;
end;
hence (idt F2)`*`t = t by A1,Th5;
now
let a be object of A;
A3: <^F1.a,F1.a^> <> {} & <^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 Th6
.= t!a by A3,ALTCAT_1:def 19;
end;
hence t`*`(idt F1) = t by A1,Th5;
end;
theorem Th8:
for A,B being category,
F,F1,F2,F3 being covariant 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 covariant Functor of A,B;
assume
A1: F is_transformable_to F1 & F1 is_transformable_to F2 &
F2 is_transformable_to F3;
let t1 be transformation of F,F1, t2 be transformation of F1,F2,
t3 be transformation of F2,F3;
A2: F is_transformable_to F2 & F1 is_transformable_to F3 by A1,Th4;
then A3: F is_transformable_to F3 by A1,Th4;
now
let a be object of A;
A4: <^F.a,F1.a^> <> {} & <^F1.a,F2.a^> <> {} & <^F2.a,F3.a^> <> {} by A1,Def1;
thus (t3`*`t2`*`t1)!a = ((t3`*`t2)!a)*(t1!a) by A1,A2,Def5
.= (t3!a)*(t2!a)*(t1!a) by A1,Def5
.= (t3!a)*((t2!a)*(t1!a)) by A4,ALTCAT_1:25
.= (t3!a)*((t2`*`t1)!a) by A1,Def5
.= (t3`*`(t2`*`t1))!a by A1,A2,Def5;
end;
hence t3`*`t2`*`t1 = t3`*`(t2`*`t1) by A3,Th5;
end;
begin :: Natural transformations
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
:Def6: 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);
end;
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^> <> {};
A2: <^a,a^> <> {} & <^b,b^> <> {} by ALTCAT_2:def 7;
let f be Morphism of a,b;
thus (idt F)!b*F.f = idm(F.b)*F.f by Th6
.= F.idm b*F.f by Th2
.= F.(idm b*f) by A1,A2,FUNCTOR0:def 24
.= F.f by A1,ALTCAT_1:24
.= F.(f*idm a) by A1,ALTCAT_1:def 19
.= F.f*F.idm a by A1,A2,FUNCTOR0:def 24
.= F.f*idm(F.a) by Th2
.= F.f*((idt F)!a) by Th6;
end;
theorem Th9:
for A,B be transitive with_units (non empty AltCatStr),
F be covariant Functor of A,B holds
F is_naturally_transformable_to F
proof
let A,B be transitive with_units (non empty AltCatStr),
F be covariant Functor of A,B;
thus F is_transformable_to F;
take idt F;
thus thesis by Lm1;
end;
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; assume
A5: <^a,b^> <> {};
then A6: <^F.a,F.b^> <> {} & <^F.b,F1.b^> <> {} by A1,Def1,FUNCTOR0:def 19;
A7: <^F.a,F1.a^> <> {} & <^F1.a,F2.a^> <> {} by A1,A2,Def1;
A8: <^F1.b,F2.b^> <> {} by A2,Def1;
A9: <^F2.a,F2.b^> <> {} by A5,FUNCTOR0:def 19;
A10: <^F1.a,F1.b^> <> {} by A5,FUNCTOR0:def 19;
let f be Morphism of a,b;
thus ((t2`*`t1)!b)*(F.f) = ((t2!b)*(t1!b))*F.f by A1,A2,Def5
.= t2!b*(t1!b*F.f) by A6,A8,ALTCAT_1:25
.= t2!b*(F1.f*(t1!a)) by A3,A5
.= t2!b*F1.f*(t1!a) by A7,A8,A10,ALTCAT_1:25
.= F2.f*(t2!a)*(t1!a) by A4,A5
.= F2.f*((t2!a)*(t1!a)) by A7,A9,ALTCAT_1:25
.= F2.f*((t2`*`t1)!a) by A1,A2,Def5;
end;
theorem Th10:
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,Th4;
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,Def6;
end;
definition
let A,B be transitive with_units (non empty AltCatStr),
F be covariant Functor of A,B;
redefine func idt F -> natural_transformation of F,F;
coherence
proof
A1: F is_naturally_transformable_to F by Th9;
idt F is natural_transformation of F,F
proof
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 A1,Def7;
end;
hence thesis;
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 and
A2: 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
A3: F is_transformable_to F1 & F1 is_transformable_to F2 by A1,A2,Def6;
A4: 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) by A1,Def7;
A5: 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 A2,Def7;
t2`*`t1 is natural_transformation of F,F2
proof
thus F is_naturally_transformable_to F2 by A1,A2,Th10;
thus thesis by A3,A4,A5,Lm2;
end;
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
proof
let A,B be transitive with_units (non empty AltCatStr),
F1,F2 be covariant Functor of A,B;
assume
F1 is_naturally_transformable_to F2;
then A1: F1 is_transformable_to F2 by Def6;
let t be natural_transformation of F1,F2;
thus (idt F2)`*`t = t by A1,Th7;
thus t`*`(idt F1) = t by A1,Th7;
end;
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)
proof
let A,B be transitive with_units (non empty AltCatStr),
F,F1,F2 be covariant Functor of A,B;
assume that
A1: F is_naturally_transformable_to F1 and
A2: F1 is_naturally_transformable_to F2;
let t1 be natural_transformation of F,F1;
let t2 be natural_transformation of F1,F2;
let a be object of A;
F is_transformable_to F1 & F1 is_transformable_to F2 by A1,A2,Def6;
hence (t2`*`t1)!a = (t2!a)*(t1!a) by Def5;
end;
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: F1 is_naturally_transformable_to F3 by A2,A3,Th10;
A5: F is_naturally_transformable_to F2 by A1,A2,Th10;
A6: F is_transformable_to F1 & F1 is_transformable_to F2 &
F2 is_transformable_to F3 by A1,A2,A3,Def6;
let t3 be natural_transformation of F2,F3;
thus t3`*`t1`*`t = t3`*`t1`*`(t qua transformation of F,F1) by A1,A4,Def8
.= (t3 qua transformation of F2,F3)`*`t1`*`t by A2,A3,Def8
.= t3`*`(t1`*`(t qua transformation of F,F1)) by A6,Th8
.= (t3 qua transformation of F2,F3)`*`(t1`*`t) by A1,A2,Def8
.= t3 `*`(t1`*`t) by A3,A5,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
assume
A1: for i being set st i in I holds B.i = {} implies A.i = {};
deffunc F(set) = Funcs(A.$1,B.$1);
consider F being ManySortedSet of I such that
A2: for i be set st i in I holds F.i = F(i) from MSSLambda;
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 set st i in dom F holds g.i in F.i by CARD_3:def 5;
A6: for i be set st i in I holds g.i is Function of A.i,B.i
proof
let i be set such that
A7: i in I;
dom F = I by PBOOLE:def 3;
then A8: g.i in F.i by A5,A7;
F.i = Funcs(A.i,B.i) by A2,A7;
hence thesis by A8,FUNCT_2:121;
end;
dom g = I by A4,PBOOLE:def 3;
then reconsider
g as ManySortedSet of I by PBOOLE:def 3;
g is ManySortedFunction of A,B by A6,MSUALG_1:def 2;
hence thesis by A3;
end;
assume
A9: x is ManySortedFunction of A,B;
then reconsider
g = x as ManySortedSet of I;
A10: dom g = I by PBOOLE:def 3;
A11: for i be set st i in I holds g.i in Funcs(A.i,B.i)
proof
let i be set; assume
A12: i in I;
then A13: g.i is Function of A.i, B.i by A9,MSUALG_1:def 2;
B.i = {} implies A.i = {} by A1,A12;
hence thesis by A13,FUNCT_2:11;
end;
A14: for i be set st i in I holds g.i in F.i
proof
let i be set; assume
A15: i in I;
then F.i = Funcs(A.i,B.i) by A2;
hence thesis by A11,A15;
end;
A16: for i be set st i in dom F holds g.i in F.i
proof
let i be set such that
A17: i in dom F;
dom F = I by PBOOLE:def 3;
hence thesis by A14,A17;
end;
dom g = dom F by A10,PBOOLE:def 3;
hence thesis by A16,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
A18: (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);
now
let x be set;
(x in it1 iff x is ManySortedFunction of A,B) &
(x in it2 iff x is ManySortedFunction of A,B) by A18;
hence x in it1 iff x in it2;
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 set holds x in it iff x is covariant strict Functor of A,B;
existence
proof
defpred R[set,set] 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;
A1: for x,y,z be set st R[x,y] & R[x,z] holds y = z
proof
let x,y,z be set;
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
A2: x = [f,m] & y = FunctorStr (#f,m#) & 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
A3: x = [f1,m1] & z = FunctorStr (#f1,m1#)
& z is covariant Functor of A,B;
f=f1 & m=m1 by A2,A3,ZFMISC_1:33;
hence y=z by A2,A3;
end;
set A' = 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 A': not contradiction};
consider f be Element of A';
(the Arrows of B)*f in sAA;
then reconsider sAA as non empty set;
defpred P[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);
A4: for x,y,z being set st P[x,y] & P[x,z] holds y = z;
consider XX being set such that
A5: for x being set holds x in XX iff
ex y being set st y in sAA & P[y,x] from Fraenkel(A4);
consider X be set such that
A6: for x be set holds x in X iff ex y be set st y in [:A',union XX:] &
R[y,x] from Fraenkel(A1);
take X;
let x be set;
thus x in X implies x is covariant strict Functor of A,B
proof
assume x in X;
then ex y be set st y in [:A',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 A6;
hence x is covariant strict Functor of A,B;
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 13;
A7: 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
A8: (the Arrows of A).(o1,o2) <> {};
(the Arrows of A).(o1,o2) = <^o1,o2^> by ALTCAT_1:def 2;
hence thesis by A8,FUNCTOR0:def 12;
end;
A9: 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
A10: (the Arrows of A).(o1,o2) <> {};
f.(o1,o2) = [F.o1,F.o2] by FUNCTOR0:23;
hence thesis by A7,A10;
end;
reconsider
m = the MorphMap of F as
MSUnTrans of f, the Arrows of A, the Arrows of B;
reconsider
y = [f,m] as set;
y in [:A',union XX:]
proof
A11: f in A' by FUNCT_2:11;
then A12: (the Arrows of B)*f in sAA;
reconsider AA = (the Arrows of B)*f
as ManySortedSet of [:the carrier of A,the carrier of A:];
set I = [:the carrier of A,the carrier of A:];
A13: m is ManySortedFunction of the Arrows of A,AA by FUNCTOR0:def 5;
A14: 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
A15: i in I and
A16: (the Arrows of A).i <> {};
consider
o1,o2 be set such that
A17: o1 in the carrier of A and
A18: o2 in the carrier of A and
A19: i = [o1,o2] by A15,ZFMISC_1:def 2;
reconsider
a1 = o1, a2 = o2 as object of A by A17,A18;
A20: (the Arrows of B).(f.i) = (the Arrows of B).(f.(o1,o2)) by A19,
BINOP_1:def 1
.= (the Arrows of B).([F.a1,F.a2]) by FUNCTOR0:23;
(the Arrows of A).(o1,o2) <> {} by A16,A19,BINOP_1:def 1;
hence thesis by A9,A20;
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
A21: i in I;
assume
A22: (the Arrows of A).i <> {};
AA.i = (the Arrows of B).(f.i) by A21,FUNCT_2:21;
hence thesis by A14,A21,A22;
end;
then (for i be set st i in I holds AA.i = {} implies (the Arrows of A).
i = {}
);
then A23: m in Funcs(the Arrows of A,AA) by A13,Def9;
Funcs(the Arrows of A,AA) in XX by A5,A12;
then m in union XX by A23,TARSKI:def 4;
hence thesis by A11,ZFMISC_1:def 2;
end;
hence x in X by A6;
end;
uniqueness
proof
let it1,it2 be set such that
A24: (for x being set holds x in it1 iff x is covariant strict Functor of A,B)&
(for x being set holds x in it2 iff x is covariant strict Functor of A,B);
now let x be set;
(x in it1 iff x is covariant strict Functor of A,B) &
(x in it2 iff x is covariant strict Functor of A,B) by A24;
hence x in it1 iff x in it2;
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 P[set,set] means
for f,g being strict covariant Functor of A,B st [f,g] = $1
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):]
ex j being set st P[i,j]
proof
let i be set; assume
i in [:Funct(A,B),Funct(A,B):];
then consider f be set,g be set such that
A2: f in Funct(A,B) & g in Funct(A,B) & i = [f,g] by ZFMISC_1:def 2;
reconsider f, g as strict covariant Functor of A,B by A2,Def10;
defpred P[set,set] means
ex o being object of A st $1 = o & $2 = <^f.o,g.o^>;
A3: for a being Element of A ex j being set st P[a,j]
proof
let a be Element of A;
reconsider
o = a as object of A;
consider j be set such that
A4: j = <^f.o,g.o^>;
thus thesis by A4;
end;
consider N being ManySortedSet of the carrier of A such that
A5: for a being Element of A holds P[a,N.a]
from MSSExD(A3);
defpred P[set] means
f is_naturally_transformable_to g & $1 is natural_transformation of f,g;
consider j being set such that
A6: for x being set holds x in j iff x in product N & P[x]
from Separation;
take j;
let f',g' be strict covariant Functor of A,B such that
A7: [f',g'] = i;
let x be set;
thus x in j implies f' is_naturally_transformable_to g' &
x is natural_transformation of f',g'
proof
assume
A8: x in j;
f' = f & g' = g by A2,A7,ZFMISC_1:33;
hence thesis by A6,A8;
end;
thus
f' is_naturally_transformable_to g' &
x is natural_transformation of f',g' implies x in j
proof
assume
A9: f' is_naturally_transformable_to g' &
x is natural_transformation of f',g';
then A10: f' is_transformable_to g' by Def6;
A11: f' = f & g' = g by A2,A7,ZFMISC_1:33;
reconsider
h = x as ManySortedSet of the carrier of A by A9;
A12: dom h = the carrier of A by PBOOLE:def 3;
set I = the carrier of A;
A13: for i' be set st i' in I holds h.i' in N.i'
proof
let i' be set; assume
i' in I;
then reconsider i' as Element of A;
consider
i'' being object of A such that
A14: i'' = i' and
A15: N.i' = <^f.i'',g.i''^> by A5;
A16: <^f.i'',g.i''^> <> {} by A10,A11,Def1;
h.i'' is Element of <^f.i'',g.i''^> by A9,A10,A11,Def2;
hence thesis by A14,A15,A16;
end;
A17: for i' be set st i' in dom N holds h.i' in N.i'
proof
let i' be set such that
A18: i' in dom N;
dom N = I by PBOOLE:def 3;
hence thesis by A13,A18;
end;
dom h = dom N by A12,PBOOLE:def 3;
then x in product N by A17,CARD_3:18;
hence thesis by A6,A9,A11;
end;
end;
consider a be ManySortedSet of [:Funct(A,B),Funct(A,B):] such that
A19: for i being set st i in [:Funct(A,B),Funct(A,B):] holds P[i,a.i]
from MSSEx(A1);
defpred Q[set,set,set] 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;
A20: for o be set st o in [:Funct(A,B),Funct(A,B),Funct(A,B):] holds
for x be set st x in {|a,a|}.o ex y be set st y in {|a|}.o & Q[y,x,o]
proof
let o be set; 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 set such that
A21: ff in [:Funct(A,B),Funct(A,B):] and
A22: h in Funct(A,B) and
A23: o = [ff,h] by ZFMISC_1:def 2;
consider
f,g be set such that
A24: f in Funct(A,B) and
A25: g in Funct(A,B) and
A26: ff = [f,g] by A21,ZFMISC_1:def 2;
A27: o = [f,g,h] by A23,A26,MCART_1:def 3;
reconsider
T = Funct(A,B) as non empty set by A22;
reconsider
i = f, j = g, k = h as Element of T by A22,A24,A25;
A28: {|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 6;
A29: {|a|}.[i,j,k] = {|a|}.(i,j,k) by MULTOP_1:def 1
.= a.(i,k) by ALTCAT_1:def 5;
for x be set st x in {|a,a|}.o ex y be set st y in {|a|}.o & Q[y,x,o]
proof
let x be set; assume
x in {|a,a|}.o;
then consider
x2,x1 be set such that
A30: x2 in a.(j,k) and
A31: x1 in a.(i,j) and
A32: x = [x2,x1] by A27,A28,ZFMISC_1:def 2;
A33: x2 in a.[j,k] by A30,BINOP_1:def 1;
A34: x1 in a.[i,j] by A31,BINOP_1:def 1;
reconsider
i' = i,j' = j, k' = k as strict covariant Functor of A,B by Def10;
A35: i' is_naturally_transformable_to j' &
x1 is natural_transformation of i',j' by A19,A34;
reconsider
x1 as natural_transformation of i',j' by A19,A34;
A36: j' is_naturally_transformable_to k' &
x2 is natural_transformation of j',k' by A19,A33;
reconsider
x2 as natural_transformation of j',k' by A19,A33;
reconsider
vv = x2 `*` x1 as natural_transformation of i',k';
A37: i' is_naturally_transformable_to k' &
vv is natural_transformation of i',k' by A35,A36,Th10;
[i',k'] in [:Funct(A,B),Funct(A,B):] by ZFMISC_1:def 2;
then vv in a.[i',k'] by A19,A37;
then A38: vv in {|a|}.o by A27,A29,BINOP_1:def 1;
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
A39: [f,g,h] = o;
let t1 be natural_transformation of f,g,
t2 be natural_transformation of g,h such that
A40: [t2,t1] = x and
ex v being Function st v.x = vv;
A41: i' = f & j' = g & k' = h by A27,A39,MCART_1:28;
then reconsider
x1 as natural_transformation of f,g;
reconsider
x2 as natural_transformation of g,h by A41;
x2 = t2 & x1 = t1 by A32,A40,ZFMISC_1:33;
hence thesis by A41;
end;
hence thesis by A38;
end;
hence thesis;
end;
consider c being ManySortedFunction of {|a,a|},{|a|} such that
A42: 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 be set st x in {|a,a|}.i holds Q[v.x,x,i] from MSFExFunc(A20);
set F = AltCatStr (#Funct(A,B),a,c #);
A43: Funct(A,B) is non empty
proof
consider f be 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;
assume
<^o1,o2^> <> {} & <^o2,o3^> <> {};
then (the Arrows of F).(o1,o2) <> {} & (the Arrows of F).(o2,o3) <> {}
by ALTCAT_1:def 2;
then A44: a.[o1,o2] <> {} & a.[o2,o3] <> {} by BINOP_1:def 1;
reconsider
a1 = o1, a2 = o2, a3 = o3 as strict covariant Functor of A,B by A43,Def10;
A45: [o1,o2] in [:Funct(A,B),Funct(A,B):] by A43,ZFMISC_1:def 2;
consider
y being set such that
A46: y in a.[o1,o2] by A44,XBOOLE_0:def 1;
A47: a1 is_naturally_transformable_to a2 &
y is natural_transformation of a1,a2 by A19,A45,A46;
reconsider y as natural_transformation of a1,a2 by A19,A45,A46;
A48: [o2,o3] in [:Funct(A,B),Funct(A,B):] by A43,ZFMISC_1:def 2;
consider x being set such that
A49: x in a.[o2,o3] by A44,XBOOLE_0:def 1;
A50: a2 is_naturally_transformable_to a3 &
x is natural_transformation of a2,a3 by A19,A48,A49;
reconsider
x as natural_transformation of a2,a3 by A19,A48,A49;
A51: x `*` y is natural_transformation of a1,a3;
A52: [o1,o3] in [:Funct(A,B),Funct(A,B):] by A43,ZFMISC_1:def 2;
a1 is_naturally_transformable_to a3 & ex x be set st
x is natural_transformation of a1,a3 by A47,A50,A51,Th10;
then a.[o1,o3] <> {} by A19,A52;
then a.(o1,o3) <> {} by BINOP_1:def 1;
hence thesis by ALTCAT_1:def 2;
end;
then reconsider F as strict non empty transitive AltCatStr by A43,STRUCT_0:
def 1;
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
assume
x in (the Arrows of F).(f,g);
then A53: x in (the Arrows of F).[f,g] by BINOP_1:def 1;
f in Funct(A,B) & g in Funct(A,B) by Def10;
then [f,g] in [:Funct(A,B),Funct(A,B):] by ZFMISC_1:def 2;
hence thesis by A19,A53;
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
assume
A54: f is_naturally_transformable_to g & x is natural_transformation of f,g
;
f in Funct(A,B) & g in Funct(A,B) by Def10;
then [f,g] in [:Funct(A,B),Funct(A,B):] by ZFMISC_1:106;
then x in a.[f,g] by A19,A54;
hence thesis by BINOP_1:def 1;
end;
end;
let f,g,h be strict covariant Functor of A,B such that
A55: f is_naturally_transformable_to g & g is_naturally_transformable_to h;
let t1 be natural_transformation of f,g,
t2 be natural_transformation of g,h;
A56: f in Funct(A,B) & g in Funct(A,B) & h in Funct(A,B) by Def10;
A57: [:Funct(A,B),Funct(A,B),Funct(A,B):] =
[:[:Funct(A,B),Funct(A,B):],Funct(A,B):] by ZFMISC_1:def 3;
A58: [f,g,h] = [[f,g],h] by MCART_1:def 3;
A59: [g,h] in [:Funct(A,B),Funct(A,B):] by A56,ZFMISC_1:106;
A60: [f,g] in [:Funct(A,B),Funct(A,B):] by A56,ZFMISC_1:106;
then [f,g,h] in
[:Funct(A,B),Funct(A,B),Funct(A,B):] by A56,A57,A58,ZFMISC_1:106;
then consider
v be Function of {|a,a|}.[f,g,h], {|a|}.[f,g,h] such that
A61: v = c.[f,g,h] and
A62: for x be set st x in {|a,a|}.[f,g,h] holds Q[v.x,x,[f,g,h]] by A42;
A63: v = c.(f,g,h) by A61,MULTOP_1:def 1;
reconsider
T = Funct(A,B) as non empty set by A56;
reconsider
i = f, j = g, k = h as Element of T by Def10;
A64: {|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 6;
A65: t1 in a.[f,g] by A19,A55,A60;
t2 in a.[g,h] by A19,A55,A59;
then t2 in a.(g,h) & t1 in a.(f,g) by A65,BINOP_1:def 1;
then [t2,t1] in {|a,a|}.[f,g,h] by A64,ZFMISC_1:106;
then v.[t2,t1] = t2`*`t1 by A62;
then v.(t2,t1) = t2`*`t1 by BINOP_1:def 1;
hence thesis by A63;
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 set st i in R & j in T holds N.(i,j) = M.(i,j)
proof
let i,j be set such that
A73: i in R and
A74: j in T;
reconsider
f = i as strict covariant Functor of A,B by A66,A73,Def10;
reconsider
g = j as strict covariant Functor of A,B by A69,A74,Def10;
now let x be set;
(x in N.(i,j) iff f is_naturally_transformable_to g &
x is natural_transformation of f,g) &
(x in M.(i,j) iff f is_naturally_transformable_to g &
x is natural_transformation of f,g) by A67,A70;
hence x in N.(i,j) iff x in M.(i,j);
end;
hence thesis by TARSKI:2;
end;
then A75: the Arrows of C1 = the Arrows of C2 by A66,A69,ALTCAT_1:8;
for i,j,k being set 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 set; assume
A76: i in R & j in R & k in R;
then reconsider
f = i as strict covariant Functor of A,B by A66,Def10;
reconsider
g = j as strict covariant Functor of A,B by A66,A76,Def10;
reconsider
h = k as strict covariant Functor of A,B by A66,A76,Def10;
per cases;
suppose
A77: N.(i,j) = {} or
N.(j,k) = {};
thus O.(i,j,k) = P.(i,j,k)
proof
per cases by A77;
suppose
N.(i,j) = {};
then A78: M.(i,j) = {} by A66,A69,A72,ALTCAT_1:8;
reconsider
T as non empty set;
reconsider
i' = i, j' = j, k' = k as Element of T by A66,A69,A76;
A79: [:M.(j',k'),M.(i',j'):] = {} by A78,ZFMISC_1:113;
A80: P.(i',j',k') is Function of [:M.(j',k'),M.(i',j'):], M.(i',k')
proof
A81: P.[i',j',k'] = P.(i',j',k') by MULTOP_1:def 1;
A82: {|M,M|}.[i',j',k'] = {|M,M|}.(i',j',k') by MULTOP_1:def 1
.= [:M.(j',k'),M.(i',j'):] by ALTCAT_1:def 6;
{|M|}.[i',j',k'] = {|M|}.(i',j',k') by MULTOP_1:def 1
.= M.(i',k') by ALTCAT_1:def 5;
hence thesis by A81,A82,MSUALG_1:def 2;
end;
O.(i',j',k') is Function of [:M.(j',k'),M.(i',j'):], M.(i',k')
proof
A83: O.[i',j',k'] = O.(i',j',k') by MULTOP_1:def 1;
A84: {|M,M|}.[i',j',k'] = {|M,M|}.(i',j',k') by MULTOP_1:def 1
.= [:M.(j',k'),M.(i',j'):] by ALTCAT_1:def 6;
{|M|}.[i',j',k'] = {|M|}.(i',j',k') by MULTOP_1:def 1
.= M.(i',k') by ALTCAT_1:def 5;
hence thesis by A66,A69,A75,A83,A84,MSUALG_1:def 2;
end; hence thesis by A79,A80,PARTFUN1:58;
suppose
N.(j,k) = {};
then A85: M.(j,k) = {} by A66,A69,A72,ALTCAT_1:8;
reconsider
T as non empty set;
reconsider
i' = i, j' = j, k' = k as Element of T by A66,A69,A76;
A86: [:M.(j',k'),M.(i',j'):] = {} by A85,ZFMISC_1:113;
A87: P.(i',j',k') is Function of [:M.(j',k'),M.(i',j'):], M.(i',k')
proof
A88: P.[i',j',k'] = P.(i',j',k') by MULTOP_1:def 1;
A89: {|M,M|}.[i',j',k'] = {|M,M|}.(i',j',k') by MULTOP_1:def 1
.= [:M.(j',k'),M.(i',j'):] by ALTCAT_1:def 6;
{|M|}.[i',j',k'] = {|M|}.(i',j',k') by MULTOP_1:def 1
.= M.(i',k') by ALTCAT_1:def 5;
hence thesis by A88,A89,MSUALG_1:def 2;
end;
O.(i',j',k') is Function of [:M.(j',k'),M.(i',j'):], M.(i',k')
proof
A90: O.[i',j',k'] = O.(i',j',k') by MULTOP_1:def 1;
A91: {|M,M|}.[i',j',k'] = {|M,M|}.(i',j',k') by MULTOP_1:def 1
.= [:M.(j',k'),M.(i',j'):] by ALTCAT_1:def 6;
{|M|}.[i',j',k'] = {|M|}.(i',j',k') by MULTOP_1:def 1
.= M.(i',k') by ALTCAT_1:def 5;
hence thesis by A66,A69,A75,A90,A91,MSUALG_1:def 2;
end; hence thesis by A86,A87,PARTFUN1:58;
end;
suppose that
A92: N.(i,j) <> {} and
A93: N.(j,k) <> {};
A94: M.(i,j) <> {} by A66,A69,A72,A92,ALTCAT_1:8;
A95: M.(j,k) <> {} by A66,A69,A72,A93,ALTCAT_1:8;
N.(i,k) <> {}
proof
reconsider
i' = i, j' = j, k' = k as object of C1 by A76;
A96: N.(i',k') = <^i',k'^> by ALTCAT_1:def 2;
A97: <^i',j'^> <> {} by A92,ALTCAT_1:def 2;
<^j',k'^> <> {} by A93,ALTCAT_1:def 2;
hence thesis by A96,A97,ALTCAT_1:def 4;
end;
then A98: M.(i,k) <> {} by A66,A69,A72,ALTCAT_1:8;
reconsider
T as non empty set;
reconsider
i' = i, j' = j, k' = k as Element of T by A66,A69,A76;
A99: P.(i,j,k) is Function of [:M.(j,k),M.(i,j):], M.(i,k)
proof
A100: P.[i',j',k'] = P.(i',j',k') by MULTOP_1:def 1;
A101: {|M,M|}.[i',j',k'] = {|M,M|}.(i',j',k') by MULTOP_1:def 1
.= [:M.(j',k'),M.(i',j'):] by ALTCAT_1:def 6;
{|M|}.[i',j',k'] = {|M|}.(i',j',k') by MULTOP_1:def 1
.= M.(i',k') by ALTCAT_1:def 5;
hence thesis by A100,A101,MSUALG_1:def 2;
end;
O.(i',j',k') is Function of [:M.(j',k'),M.(i',j'):], M.(i',k')
proof
A102: O.[i',j',k'] = O.(i',j',k') by MULTOP_1:def 1;
A103: {|M,M|}.[i',j',k'] = {|M,M|}.(i',j',k') by MULTOP_1:def 1
.= [:M.(j',k'),M.(i',j'):] by ALTCAT_1:def 6;
{|M|}.[i',j',k'] = {|M|}.(i',j',k') by MULTOP_1:def 1
.= M.(i',k') by ALTCAT_1:def 5;
hence thesis by A66,A69,A75,A102,A103,MSUALG_1:def 2;
end;
then reconsider
t1 = O.(i,j,k) as Function of [:M.(j,k),M.(i,j):], M.(i,k);
reconsider
t2 = P.(i,j,k) as Function of [:M.(j,k),M.(i,j):], M.(i,k) by A99;
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 A95;
then A104: g is_naturally_transformable_to h &
a is natural_transformation of g,h by A70;
reconsider
a as natural_transformation of g,h by A70,A95;
b in M.(i,j) by A94;
then A105: f is_naturally_transformable_to g &
b is natural_transformation of f,g by A70;
reconsider
b as natural_transformation of f,g by A70,A94;
consider
t1' be Function such that
A106: t1' = O.(f,g,h) and
A107: t1'.(a,b) = a `*` b by A68,A104,A105;
consider
t2' be Function such that
A108: t2' = P.(f,g,h) and
A109: t2'.(a,b) = a `*` b by A71,A104,A105;
thus thesis by A106,A107,A108,A109;
end;
hence thesis by A94,A95,A98,BINOP_1:2;
end;
hence C1 = C2 by A66,A69,A75,ALTCAT_1:10;
end;
end;