let I be set ; for E being non empty set
for A being ObjectsFamily of I,(EnsCat E) st product A in E holds
( EnsCatProduct A is feasible & EnsCatProduct A is projection-morphisms )
let E be non empty set ; for A being ObjectsFamily of I,(EnsCat E) st product A in E holds
( EnsCatProduct A is feasible & EnsCatProduct A is projection-morphisms )
let A be ObjectsFamily of I,(EnsCat E); ( product A in E implies ( EnsCatProduct A is feasible & EnsCatProduct A is projection-morphisms ) )
set B = EnsCatProductObj A;
set P = EnsCatProduct A;
assume A1:
product A in E
; ( EnsCatProduct A is feasible & EnsCatProduct A is projection-morphisms )
then A2:
EnsCatProductObj A = product A
by Def10;
per cases
( product A <> {} or product A = {} )
;
suppose A3:
product A <> {}
;
( EnsCatProduct A is feasible & EnsCatProduct A is projection-morphisms )A4:
dom A = I
by PARTFUN1:def 2;
thus
EnsCatProduct A is
feasible
EnsCatProduct A is projection-morphisms proof
let i be
set ;
ALTCAT_5:def 4 ( i in I implies ex o being Object of (EnsCat E) st
( o = A . i & (EnsCatProduct A) . i in <^(EnsCatProductObj A),o^> ) )
assume A6:
i in I
;
ex o being Object of (EnsCat E) st
( o = A . i & (EnsCatProduct A) . i in <^(EnsCatProductObj A),o^> )
then reconsider I =
I as non
empty set ;
reconsider i =
i as
Element of
I by A6;
reconsider A =
A as
ObjectsFamily of
I,
(EnsCat E) ;
reconsider P =
EnsCatProduct A as
MorphismsFamily of
EnsCatProductObj A,
A ;
take
A . i
;
( A . i = A . i & (EnsCatProduct A) . i in <^(EnsCatProductObj A),(A . i)^> )
A7:
<^(EnsCatProductObj A),(A . i)^> = Funcs (
(EnsCatProductObj A),
(A . i))
by ALTCAT_1:def 14;
A . i <> {}
by A5;
then
Funcs (
(EnsCatProductObj A),
(A . i))
<> {}
;
then
P . i in <^(EnsCatProductObj A),(A . i)^>
by A7;
hence
(
A . i = A . i &
(EnsCatProduct A) . i in <^(EnsCatProductObj A),(A . i)^> )
;
verum
end; let X be
Object of
(EnsCat E);
ALTCAT_5:def 6 for F being MorphismsFamily of X,A st F is feasible holds
ex f being Morphism of X,(EnsCatProductObj A) st
( f in <^X,(EnsCatProductObj A)^> & ( for i being set st i in I holds
ex si being Object of (EnsCat E) ex Pi being Morphism of (EnsCatProductObj A),si st
( si = A . i & Pi = (EnsCatProduct A) . i & F . i = Pi * f ) ) & ( for f1 being Morphism of X,(EnsCatProductObj A) st ( for i being set st i in I holds
ex si being Object of (EnsCat E) ex Pi being Morphism of (EnsCatProductObj A),si st
( si = A . i & Pi = (EnsCatProduct A) . i & F . i = Pi * f1 ) ) holds
f = f1 ) )let F be
MorphismsFamily of
X,
A;
( F is feasible implies ex f being Morphism of X,(EnsCatProductObj A) st
( f in <^X,(EnsCatProductObj A)^> & ( for i being set st i in I holds
ex si being Object of (EnsCat E) ex Pi being Morphism of (EnsCatProductObj A),si st
( si = A . i & Pi = (EnsCatProduct A) . i & F . i = Pi * f ) ) & ( for f1 being Morphism of X,(EnsCatProductObj A) st ( for i being set st i in I holds
ex si being Object of (EnsCat E) ex Pi being Morphism of (EnsCatProductObj A),si st
( si = A . i & Pi = (EnsCatProduct A) . i & F . i = Pi * f1 ) ) holds
f = f1 ) ) )assume
F is
feasible
;
ex f being Morphism of X,(EnsCatProductObj A) st
( f in <^X,(EnsCatProductObj A)^> & ( for i being set st i in I holds
ex si being Object of (EnsCat E) ex Pi being Morphism of (EnsCatProductObj A),si st
( si = A . i & Pi = (EnsCatProduct A) . i & F . i = Pi * f ) ) & ( for f1 being Morphism of X,(EnsCatProductObj A) st ( for i being set st i in I holds
ex si being Object of (EnsCat E) ex Pi being Morphism of (EnsCatProductObj A),si st
( si = A . i & Pi = (EnsCatProduct A) . i & F . i = Pi * f1 ) ) holds
f = f1 ) )A8:
<^X,(EnsCatProductObj A)^> = Funcs (
X,
(EnsCatProductObj A))
by ALTCAT_1:def 14;
defpred S1[
object ,
object ]
means ex
M being
ManySortedSet of
I st
( ( for
i being
set st
i in I holds
M . i = (F . i) . $1 ) & $2
= M );
A9:
for
x being
object st
x in X holds
ex
u being
object st
S1[
x,
u]
consider ff being
Function such that A11:
dom ff = X
and A12:
for
x being
object st
x in X holds
S1[
x,
ff . x]
from CLASSES1:sch 1(A9);
A13:
rng ff c= EnsCatProductObj A
then reconsider ff =
ff as
Morphism of
X,
(EnsCatProductObj A) by A8, A11, FUNCT_2:def 2;
take
ff
;
( ff in <^X,(EnsCatProductObj A)^> & ( for i being set st i in I holds
ex si being Object of (EnsCat E) ex Pi being Morphism of (EnsCatProductObj A),si st
( si = A . i & Pi = (EnsCatProduct A) . i & F . i = Pi * ff ) ) & ( for f1 being Morphism of X,(EnsCatProductObj A) st ( for i being set st i in I holds
ex si being Object of (EnsCat E) ex Pi being Morphism of (EnsCatProductObj A),si st
( si = A . i & Pi = (EnsCatProduct A) . i & F . i = Pi * f1 ) ) holds
ff = f1 ) )thus A23:
ff in <^X,(EnsCatProductObj A)^>
by A8, A13, A11, FUNCT_2:def 2;
( ( for i being set st i in I holds
ex si being Object of (EnsCat E) ex Pi being Morphism of (EnsCatProductObj A),si st
( si = A . i & Pi = (EnsCatProduct A) . i & F . i = Pi * ff ) ) & ( for f1 being Morphism of X,(EnsCatProductObj A) st ( for i being set st i in I holds
ex si being Object of (EnsCat E) ex Pi being Morphism of (EnsCatProductObj A),si st
( si = A . i & Pi = (EnsCatProduct A) . i & F . i = Pi * f1 ) ) holds
ff = f1 ) )thus
for
i being
set st
i in I holds
ex
si being
Object of
(EnsCat E) ex
Pi being
Morphism of
(EnsCatProductObj A),
si st
(
si = A . i &
Pi = (EnsCatProduct A) . i &
F . i = Pi * ff )
for f1 being Morphism of X,(EnsCatProductObj A) st ( for i being set st i in I holds
ex si being Object of (EnsCat E) ex Pi being Morphism of (EnsCatProductObj A),si st
( si = A . i & Pi = (EnsCatProduct A) . i & F . i = Pi * f1 ) ) holds
ff = f1proof
let i be
set ;
( i in I implies ex si being Object of (EnsCat E) ex Pi being Morphism of (EnsCatProductObj A),si st
( si = A . i & Pi = (EnsCatProduct A) . i & F . i = Pi * ff ) )
assume A24:
i in I
;
ex si being Object of (EnsCat E) ex Pi being Morphism of (EnsCatProductObj A),si st
( si = A . i & Pi = (EnsCatProduct A) . i & F . i = Pi * ff )
then reconsider I =
I as non
empty set ;
reconsider j =
i as
Element of
I by A24;
reconsider A1 =
A as
ObjectsFamily of
I,
(EnsCat E) ;
reconsider P1 =
EnsCatProduct A as
MorphismsFamily of
EnsCatProductObj A,
A1 ;
reconsider F1 =
F as
MorphismsFamily of
X,
A1 ;
take
A1 . j
;
ex Pi being Morphism of (EnsCatProductObj A),(A1 . j) st
( A1 . j = A . i & Pi = (EnsCatProduct A) . i & F . i = Pi * ff )
take
P1 . j
;
( A1 . j = A . i & P1 . j = (EnsCatProduct A) . i & F . i = (P1 . j) * ff )
thus
(
A1 . j = A . i &
P1 . j = (EnsCatProduct A) . i )
;
F . i = (P1 . j) * ff
reconsider p =
P1 . j as
Function ;
A25:
<^(EnsCatProductObj A),(A1 . j)^> = Funcs (
(EnsCatProductObj A),
(A1 . j))
by ALTCAT_1:def 14;
A26:
A1 . j <> {}
by A5;
then
<^X,(A1 . j)^> <> {}
by A25, A23, ALTCAT_1:def 2;
then A27:
(P1 . j) * ff = p * ff
by A23, A26, A25, ALTCAT_1:16;
A28:
<^X,(A1 . j)^> = Funcs (
X,
(A1 . j))
by ALTCAT_1:def 14;
then A29:
dom ((P1 . j) * ff) = X
by A26, FUNCT_2:92;
A30:
dom (F1 . j) = X
by A26, A28, FUNCT_2:92;
now for x being object st x in dom (F1 . j) holds
(p * ff) . x = (F1 . j) . xlet x be
object ;
( x in dom (F1 . j) implies (p * ff) . x = (F1 . j) . x )assume A31:
x in dom (F1 . j)
;
(p * ff) . x = (F1 . j) . xthen consider M being
ManySortedSet of
I such that A32:
for
i being
set st
i in I holds
M . i = (F . i) . x
and A33:
ff . x = M
by A12, A30;
A34:
dom (proj (A,j)) = EnsCatProductObj A
by A2, CARD_3:def 16;
A35:
ff . x in rng ff
by A11, A30, A31, FUNCT_1:def 3;
thus (p * ff) . x =
p . (ff . x)
by A11, A30, A31, FUNCT_1:13
.=
(proj (A,j)) . (ff . x)
by A1, Def11
.=
M . j
by A33, A34, A35, A13, CARD_3:def 16
.=
(F1 . j) . x
by A32
;
verum end;
hence
F . i = (P1 . j) * ff
by A27, A29, A26, A28, FUNCT_2:92, FUNCT_1:2;
verum
end; let f1 be
Morphism of
X,
(EnsCatProductObj A);
( ( for i being set st i in I holds
ex si being Object of (EnsCat E) ex Pi being Morphism of (EnsCatProductObj A),si st
( si = A . i & Pi = (EnsCatProduct A) . i & F . i = Pi * f1 ) ) implies ff = f1 )assume A36:
for
i being
set st
i in I holds
ex
si being
Object of
(EnsCat E) ex
Pi being
Morphism of
(EnsCatProductObj A),
si st
(
si = A . i &
Pi = (EnsCatProduct A) . i &
F . i = Pi * f1 )
;
ff = f1A37:
f1 is
Function of
X,
(EnsCatProductObj A)
by A8, A23, FUNCT_2:66;
then A38:
dom f1 = X
by A3, A2, FUNCT_2:def 1;
A39:
rng f1 c= EnsCatProductObj A
by A37, RELAT_1:def 19;
now for x being object st x in dom ff holds
ff . x = f1 . xlet x be
object ;
( x in dom ff implies ff . x = f1 . x )assume A40:
x in dom ff
;
ff . x = f1 . xthen A41:
f1 . x in rng f1
by A11, A38, FUNCT_1:def 3;
reconsider h =
f1 . x as
Function by A2, A37;
consider M being
ManySortedSet of
I such that A42:
for
i being
set st
i in I holds
M . i = (F . i) . x
and A43:
ff . x = M
by A11, A12, A40;
A44:
dom h = I
by A2, A4, A41, A39, CARD_3:9;
now for i being object st i in dom M holds
M . i = h . ilet i be
object ;
( i in dom M implies M . i = h . i )assume A45:
i in dom M
;
M . i = h . ithen consider si being
Object of
(EnsCat E),
Pi being
Morphism of
(EnsCatProductObj A),
si such that A46:
(
si = A . i &
Pi = (EnsCatProduct A) . i )
and A47:
F . i = Pi * f1
by A36;
A48:
(EnsCatProduct A) . i = proj (
A,
i)
by A1, A45, Def11;
A49:
dom (proj (A,i)) = EnsCatProductObj A
by A2, CARD_3:def 16;
A50:
<^(EnsCatProductObj A),si^> = Funcs (
(EnsCatProductObj A),
si)
by ALTCAT_1:def 14;
A51:
si <> {}
by A5, A45, A46;
then A52:
<^X,si^> <> {}
by A50, A23, ALTCAT_1:def 2;
thus M . i =
(Pi * f1) . x
by A47, A42, A45
.=
(Pi * f1) . x
by A50, A23, A51, A52, ALTCAT_1:16
.=
Pi . h
by A38, A11, A40, FUNCT_1:13
.=
h . i
by A39, A41, A46, A48, A49, CARD_3:def 16
;
verum end; hence
ff . x = f1 . x
by A44, A43, FUNCT_1:2, PARTFUN1:def 2;
verum end; hence
ff = f1
by A11, A38, FUNCT_1:2;
verum end; suppose A53:
product A = {}
;
( EnsCatProduct A is feasible & EnsCatProduct A is projection-morphisms )thus
EnsCatProduct A is
feasible
EnsCatProduct A is projection-morphisms proof
let i be
set ;
ALTCAT_5:def 4 ( i in I implies ex o being Object of (EnsCat E) st
( o = A . i & (EnsCatProduct A) . i in <^(EnsCatProductObj A),o^> ) )
assume A54:
i in I
;
ex o being Object of (EnsCat E) st
( o = A . i & (EnsCatProduct A) . i in <^(EnsCatProductObj A),o^> )
reconsider I =
I as non
empty set by A54;
reconsider i =
i as
Element of
I by A54;
reconsider A =
A as
ObjectsFamily of
I,
(EnsCat E) ;
take
A . i
;
( A . i = A . i & (EnsCatProduct A) . i in <^(EnsCatProductObj A),(A . i)^> )
A55:
<^(EnsCatProductObj A),(A . i)^> =
Funcs (
(EnsCatProductObj A),
(A . i))
by ALTCAT_1:def 14
.=
{{}}
by A2, A53, FUNCT_5:57
;
(EnsCatProduct A) . i =
(I --> {}) . i
by A1, A53, Th7
.=
{}
;
hence
(
A . i = A . i &
(EnsCatProduct A) . i in <^(EnsCatProductObj A),(A . i)^> )
by A55, TARSKI:def 1;
verum
end; let X be
Object of
(EnsCat E);
ALTCAT_5:def 6 for F being MorphismsFamily of X,A st F is feasible holds
ex f being Morphism of X,(EnsCatProductObj A) st
( f in <^X,(EnsCatProductObj A)^> & ( for i being set st i in I holds
ex si being Object of (EnsCat E) ex Pi being Morphism of (EnsCatProductObj A),si st
( si = A . i & Pi = (EnsCatProduct A) . i & F . i = Pi * f ) ) & ( for f1 being Morphism of X,(EnsCatProductObj A) st ( for i being set st i in I holds
ex si being Object of (EnsCat E) ex Pi being Morphism of (EnsCatProductObj A),si st
( si = A . i & Pi = (EnsCatProduct A) . i & F . i = Pi * f1 ) ) holds
f = f1 ) )let F be
MorphismsFamily of
X,
A;
( F is feasible implies ex f being Morphism of X,(EnsCatProductObj A) st
( f in <^X,(EnsCatProductObj A)^> & ( for i being set st i in I holds
ex si being Object of (EnsCat E) ex Pi being Morphism of (EnsCatProductObj A),si st
( si = A . i & Pi = (EnsCatProduct A) . i & F . i = Pi * f ) ) & ( for f1 being Morphism of X,(EnsCatProductObj A) st ( for i being set st i in I holds
ex si being Object of (EnsCat E) ex Pi being Morphism of (EnsCatProductObj A),si st
( si = A . i & Pi = (EnsCatProduct A) . i & F . i = Pi * f1 ) ) holds
f = f1 ) ) )assume A56:
F is
feasible
;
ex f being Morphism of X,(EnsCatProductObj A) st
( f in <^X,(EnsCatProductObj A)^> & ( for i being set st i in I holds
ex si being Object of (EnsCat E) ex Pi being Morphism of (EnsCatProductObj A),si st
( si = A . i & Pi = (EnsCatProduct A) . i & F . i = Pi * f ) ) & ( for f1 being Morphism of X,(EnsCatProductObj A) st ( for i being set st i in I holds
ex si being Object of (EnsCat E) ex Pi being Morphism of (EnsCatProductObj A),si st
( si = A . i & Pi = (EnsCatProduct A) . i & F . i = Pi * f1 ) ) holds
f = f1 ) )A61:
<^X,(EnsCatProductObj A)^> =
Funcs (
X,
(EnsCatProductObj A))
by ALTCAT_1:def 14
.=
{{}}
by A57, FUNCT_5:57
;
then reconsider f =
{} as
Morphism of
X,
(EnsCatProductObj A) by TARSKI:def 1;
take
f
;
( f in <^X,(EnsCatProductObj A)^> & ( for i being set st i in I holds
ex si being Object of (EnsCat E) ex Pi being Morphism of (EnsCatProductObj A),si st
( si = A . i & Pi = (EnsCatProduct A) . i & F . i = Pi * f ) ) & ( for f1 being Morphism of X,(EnsCatProductObj A) st ( for i being set st i in I holds
ex si being Object of (EnsCat E) ex Pi being Morphism of (EnsCatProductObj A),si st
( si = A . i & Pi = (EnsCatProduct A) . i & F . i = Pi * f1 ) ) holds
f = f1 ) )thus
f in <^X,(EnsCatProductObj A)^>
by A61;
( ( for i being set st i in I holds
ex si being Object of (EnsCat E) ex Pi being Morphism of (EnsCatProductObj A),si st
( si = A . i & Pi = (EnsCatProduct A) . i & F . i = Pi * f ) ) & ( for f1 being Morphism of X,(EnsCatProductObj A) st ( for i being set st i in I holds
ex si being Object of (EnsCat E) ex Pi being Morphism of (EnsCatProductObj A),si st
( si = A . i & Pi = (EnsCatProduct A) . i & F . i = Pi * f1 ) ) holds
f = f1 ) )thus
for
i being
set st
i in I holds
ex
si being
Object of
(EnsCat E) ex
Pi being
Morphism of
(EnsCatProductObj A),
si st
(
si = A . i &
Pi = (EnsCatProduct A) . i &
F . i = Pi * f )
for f1 being Morphism of X,(EnsCatProductObj A) st ( for i being set st i in I holds
ex si being Object of (EnsCat E) ex Pi being Morphism of (EnsCatProductObj A),si st
( si = A . i & Pi = (EnsCatProduct A) . i & F . i = Pi * f1 ) ) holds
f = f1proof
let i be
set ;
( i in I implies ex si being Object of (EnsCat E) ex Pi being Morphism of (EnsCatProductObj A),si st
( si = A . i & Pi = (EnsCatProduct A) . i & F . i = Pi * f ) )
assume A62:
i in I
;
ex si being Object of (EnsCat E) ex Pi being Morphism of (EnsCatProductObj A),si st
( si = A . i & Pi = (EnsCatProduct A) . i & F . i = Pi * f )
reconsider J =
I as non
empty set by A62;
reconsider j =
i as
Element of
J by A62;
reconsider A1 =
A as
ObjectsFamily of
J,
(EnsCat E) ;
reconsider P1 =
EnsCatProduct A as
MorphismsFamily of
EnsCatProductObj A,
A1 ;
reconsider si =
A1 . j as
Object of
(EnsCat E) ;
reconsider Pi =
P1 . j as
Morphism of
(EnsCatProductObj A),
si ;
reconsider F1 =
F as
MorphismsFamily of
X,
A1 ;
reconsider F2 =
F1 . j as
Morphism of
X,
si ;
take
si
;
ex Pi being Morphism of (EnsCatProductObj A),si st
( si = A . i & Pi = (EnsCatProduct A) . i & F . i = Pi * f )
take
Pi
;
( si = A . i & Pi = (EnsCatProduct A) . i & F . i = Pi * f )
thus
(
si = A . i &
Pi = (EnsCatProduct A) . i )
;
F . i = Pi * f
A63:
<^(EnsCatProductObj A),si^> =
Funcs (
(EnsCatProductObj A),
si)
by ALTCAT_1:def 14
.=
{{}}
by A2, A53, FUNCT_5:57
;
then A64:
<^X,si^> <> {}
by A61, ALTCAT_1:def 2;
A65:
Funcs (
X,
si)
= {{}}
by A57, FUNCT_5:57;
A66:
<^X,si^> = Funcs (
X,
si)
by ALTCAT_1:def 14;
thus F . i =
F2
.=
{}
by A65, A66, TARSKI:def 1
.=
Pi * f
.=
Pi * f
by A63, A61, A64, ALTCAT_1:16
;
verum
end; let f1 be
Morphism of
X,
(EnsCatProductObj A);
( ( for i being set st i in I holds
ex si being Object of (EnsCat E) ex Pi being Morphism of (EnsCatProductObj A),si st
( si = A . i & Pi = (EnsCatProduct A) . i & F . i = Pi * f1 ) ) implies f = f1 )thus
( ( for
i being
set st
i in I holds
ex
si being
Object of
(EnsCat E) ex
Pi being
Morphism of
(EnsCatProductObj A),
si st
(
si = A . i &
Pi = (EnsCatProduct A) . i &
F . i = Pi * f1 ) ) implies
f = f1 )
by A61, TARSKI:def 1;
verum end; end;