let I be set ; :: thesis:
let E be non empty set ; :: thesis:
let A be ObjectsFamily of I,(EnsCat E); :: thesis:
set B = EnsCatProductObj A;
set P = EnsCatProduct A;
assume A1: product A in E ; :: thesis:
then A2: EnsCatProductObj A = product A by Def10;

per cases ;

suppose A3: product A <> {} ; :: thesis:

A4: dom A = I by PARTFUN1:def 2;

A5: now :: thesis:

let i be set ; :: thesis:
assume i in I ; :: thesis:
then A . i in rng A by A4, FUNCT_1:def 3;
hence A . i <> {} by A3, CARD_3:26; :: thesis:

end;

thus EnsCatProduct A is feasible :: thesis:

proof

let i be set ; :: according to ALTCAT_5:def 4 :: thesis:
assume A6: i in I ; :: thesis:
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 ; :: thesis:
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)^> ) ; :: thesis:

end;

let X be Object of (EnsCat E); :: according to ALTCAT_5:def 6 :: thesis:
let F be MorphismsFamily of X,A; :: thesis:
assume F is feasible ; :: thesis:
A8: <^X,(EnsCatProductObj A)^> = Funcs (X,(EnsCatProductObj A)) by ALTCAT_1:def 14;
defpred S₁[ 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 S₁[x,u]

proof

let x be object ; :: thesis:
assume x in X ; :: thesis:
deffunc H₁( object ) -> set = (F . $1) . x;
consider f being ManySortedSet of I such that
A10: for i being object st i in I holds
f . i = H₁(i) from PBOOLE:sch 4();
take f ; :: thesis:
take f ; :: thesis:
thus ( ( for i being set st i in I holds
f . i = (F . i) . x ) & f = f ) by A10; :: thesis:

end;

consider ff being Function such that
A11: dom ff = X and
A12: for x being object st x in X holds
S₁[x,ff . x] from CLASSES1:sch 1(A9);
A13: rng ff c= EnsCatProductObj A

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng ff ; :: thesis:
then consider x being object such that
A14: x in dom ff and
A15: ff . x = y by FUNCT_1:def 3;
consider M being ManySortedSet of I such that
A16: for i being set st i in I holds
M . i = (F . i) . x and
A17: ff . x = M by A11, A12, A14;
A18: dom M = I by PARTFUN1:def 2;

now :: thesis:

let i be object ; :: thesis:
assume A19: i in dom A ; :: thesis:
then reconsider I = I as non empty set ;
reconsider j = i as Element of I by A19;
reconsider A1 = A as ObjectsFamily of I,(EnsCat E) ;
reconsider F1 = F as MorphismsFamily of X,A1 ;
A20: <^X,(A1 . j)^> = Funcs (X,(A1 . j)) by ALTCAT_1:def 14;
A1 . j <> {} by A5;
then A21: ( dom (F1 . j) = X & rng (F1 . j) c= A1 . j ) by A20, FUNCT_2:92;
then A22: (F1 . j) . x in rng (F1 . j) by A14, A11, FUNCT_1:def 3;
M . j = (F . j) . x by A16;
hence M . i in A . i by A22, A21; :: thesis:

end;

hence y in EnsCatProductObj A by A2, A4, A15, A17, A18, CARD_3:9; :: thesis:

end;

then reconsider ff = ff as Morphism of X,(EnsCatProductObj A) by A8, A11, FUNCT_2:def 2;
take ff ; :: thesis:
thus A23: ff in <^X,(EnsCatProductObj A)^> by A8, A13, A11, FUNCT_2:def 2; :: thesis:
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 ) :: thesis:

proof

let i be set ; :: thesis:
assume A24: i in I ; :: thesis:
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 ; :: thesis:
take P1 . j ; :: thesis:
thus ( A1 . j = A . i & P1 . j = (EnsCatProduct A) . i ) ; :: thesis:
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 :: thesis:

let x be object ; :: thesis:
assume A31: x in dom (F1 . j) ; :: thesis:
then 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 ; :: thesis:

end;

hence F . i = (P1 . j) * ff by A27, A29, A26, A28, FUNCT_2:92, FUNCT_1:2; :: thesis:

end;

let f1 be Morphism of X,(EnsCatProductObj A); :: thesis:
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 ) ; :: thesis:
A37: 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 :: thesis:

let x be object ; :: thesis:
assume A40: x in dom ff ; :: thesis:
then 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 :: thesis:

let i be object ; :: thesis:
assume A45: i in dom M ; :: thesis:
then 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 ; :: thesis:

end;

hence ff . x = f1 . x by A44, A43, FUNCT_1:2, PARTFUN1:def 2; :: thesis:

end;

hence ff = f1 by A11, A38, FUNCT_1:2; :: thesis:

end;

suppose A53: product A = {} ; :: thesis:

thus EnsCatProduct A is feasible :: thesis:

proof

let i be set ; :: according to ALTCAT_5:def 4 :: thesis:
assume A54: i in I ; :: thesis:
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 ; :: thesis:
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; :: thesis:

end;

let X be Object of (EnsCat E); :: according to ALTCAT_5:def 6 :: thesis:
let F be MorphismsFamily of X,A; :: thesis:
assume A56: F is feasible ; :: thesis:

A57: now :: thesis:

assume A58: X <> {} ; :: thesis:
{} in rng A by A53, CARD_3:26;
then consider i being object such that
A59: i in dom A and
A60: A . i = {} by FUNCT_1:def 3;
reconsider I = I as non empty set by A59;
reconsider i = i as Element of I by A59;
reconsider A = A as ObjectsFamily of I,(EnsCat E) ;
<^X,(A . i)^> = Funcs (X,(A . i)) by ALTCAT_1:def 14
.= {} by A58, A60 ;
hence contradiction by A56, Def5; :: thesis:

end;

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 ; :: thesis:
thus f in <^X,(EnsCatProductObj A)^> by A61; :: thesis:
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 ) :: thesis:

proof

let i be set ; :: thesis:
assume A62: i in I ; :: thesis:
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 ; :: thesis:
take Pi ; :: thesis:
thus ( si = A . i & Pi = (EnsCatProduct A) . i ) ; :: thesis:
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 ; :: thesis:

end;

let f1 be Morphism of X,(EnsCatProductObj A); :: thesis:
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; :: thesis:

end;