begin
scheme
FuncIdxcorrectness{
F1()
-> set ,
F2()
-> non
empty set ,
F3(
set )
-> Element of
F2() } :
( ex
F being
Function of
F1(),
F2() st
for
x being
set st
x in F1() holds
F /. x = F3(
x) & ( for
F1,
F2 being
Function of
F1(),
F2() st ( for
x being
set st
x in F1() holds
F1 /. x = F3(
x) ) & ( for
x being
set st
x in F1() holds
F2 /. x = F3(
x) ) holds
F1 = F2 ) )
theorem Th3:
for
x1,
x2 being
set for
A being non
empty set st
x1 <> x2 holds
for
y1,
y2 being
Element of
A holds
(
((x1,x2) --> (y1,y2)) /. x1 = y1 &
((x1,x2) --> (y1,y2)) /. x2 = y2 )
begin
theorem
for
x1,
x2 being
set for
C being
Category for
p1,
p2,
q1,
q2 being
Morphism of
C st
x1 <> x2 holds
((x1,x2) --> (p1,p2)) "*" ((x1,x2) --> (q1,q2)) = (
x1,
x2)
--> (
(p1 (*) q1),
(p2 (*) q2))
begin
Lm1:
for C, D being Category
for T being Functor of C,D
for a, b, c being Object of C st Hom (a,b) <> {} & Hom (b,c) <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds T /. (g * f) = (T /. g) * (T /. f)
Lm2:
for C, D being Category
for T being Functor of C,D
for c being Object of C holds T /. (id c) = id (T . c)
begin
begin
begin
theorem
for
C being
Category for
c,
a,
b being
Object of
C st
Hom (
c,
a)
<> {} &
Hom (
c,
b)
<> {} holds
for
p1 being
Morphism of
c,
a for
p2 being
Morphism of
c,
b holds
(
c is_a_product_wrt p1,
p2 iff for
d being
Object of
C st
Hom (
d,
a)
<> {} &
Hom (
d,
b)
<> {} holds
(
Hom (
d,
c)
<> {} & ( for
f being
Morphism of
d,
a for
g being
Morphism of
d,
b ex
h being
Morphism of
d,
c st
for
k being
Morphism of
d,
c holds
( (
p1 * k = f &
p2 * k = g ) iff
h = k ) ) ) )
begin
theorem
for
C being
Category for
a,
c,
b being
Object of
C st
Hom (
a,
c)
<> {} &
Hom (
b,
c)
<> {} holds
for
i1 being
Morphism of
a,
c for
i2 being
Morphism of
b,
c holds
(
c is_a_coproduct_wrt i1,
i2 iff for
d being
Object of
C st
Hom (
a,
d)
<> {} &
Hom (
b,
d)
<> {} holds
(
Hom (
c,
d)
<> {} & ( for
f being
Morphism of
a,
d for
g being
Morphism of
b,
d ex
h being
Morphism of
c,
d st
for
k being
Morphism of
c,
d holds
( (
k * i1 = f &
k * i2 = g ) iff
h = k ) ) ) )