Database Reference
In-Depth Information
=
1
≤
j
≤
m
A
j
,
B
=
1
≤
i
≤
k
B
i
and
C
=
1
≤
l
≤
n
C
l
with
m,k,n
Proof
Let
A
≥
1.
f
Then, for any ptp arrow
(f
ji
:
A
j
→
B
i
)
∈
we define the set of indexes:
l
|
.
g
in
L
ji
=
1
≤
l
≤
n,(g
jl
:
A
j
→
C
l
)
∈
and
(in
li
:
C
l
→
B
i
)
∈
f
Consequently, from the fact that
f
=
in
◦
g
, for each ptp arrow
f
ji
∈
the following
must hold:
(i)
f
ji
=
T(
{
in
li
◦
g
jl
|
l
∈
L
ij
}
)
=
T(
{
in
li
∩
g
jl
|
l
∈
L
ij
}
)
=
T(
{
TC
l
∩
T(
{
g
jl
|
∈
L
ij
}
=
g
jl
|
∈
L
ij
}
l
)
l
)
, and hence
g
jl
⊆
f
ji
for each
l
(ii)
L
ij
.
From the fact that it holds for every
f
ji
, we can define an arrow
k
∈
:
f
→
C
as
follows:
for each
(f
ji
:
A
j
→
B
i
)
∈
f
, we define a ptp arrow for each
l
∈
L
ij
,
k
jil
:
f
ji
→
C
l
such that
(iii)
k
jil
=
g
jl
.
Let us show that
g
=
k
◦
τ
J(f)
, that is, for each ptp arrow
(g
jl
:
A
j
→
C
l
)
∈
T(
{
g
A
j
→
f
ji
)
,wehavethat
g
jl
=
k
jil
◦
τ
J(f
ji
)
|
1
≤
i
≤
k,(τ
J(f
ji
)
:
∈
τ
J(f)
and
(k
jil
:
f
ji
→
k
C
l
)
∈
}
)
. Indeed,
T
τ
J(f)
k
k
jil
◦
τ
J(f
ji
)
|
1
≤
i
≤
k,τ
J(f
ji
)
∈
and
k
jil
∈
=
T
τ
J(f)
k
k
jil
∩
τ
J(f
ji
)
|
1
≤
i
≤
k,τ
J(f
ji
)
∈
and
k
jil
∈
(from (iii))
T
τ
J(f)
k
=
g
jl
∩
τ
J(f
ji
)
|
1
≤
i
≤
k,τ
J(f
ji
)
∈
and
k
jil
∈
T
τ
J(f)
k
=
g
jl
|
1
≤
i
≤
k,τ
J(f
ji
)
∈
and
k
jil
∈
(from
f
ji
=
τ
J(f
ji
)
and (ii))
=
T
g
jl
=
g
jl
.
Finally, let us show that
τ
−
1
J(f)
=
in
◦
k
, that is, for each ptp monic arrow
T(
{
τ
−
1
J(f)
,
τ
−
1
(τ
−
1
J(f
ji
)
:
f
ji
n,(k
jil
:
f
ji
→
→
B
i
)
∈
J(f
ji
)
=
in
li
◦
k
jil
|
1
≤
l
≤
k
in
C
l
)
∈
and
(in
li
:
C
l
→
B
i
)
∈
}
)
. Indeed,
T
k
in
in
li
◦
k
jil
|
1
≤
l
≤
n,k
jil
∈
and
in
li
∈
T
k
in
in
li
∩
k
jil
|
=
1
≤
l
≤
n,k
jil
∈
and
in
li
∈
