let I be set ; :: thesis:
let E be non empty set ; :: thesis:
let A be ObjectsFamily of I,(EnsCat E); :: thesis:
set B = EnsCatCoproductObj A;
set P = EnsCatCoproduct A;
assume A1: Union (coprod A) in E ; :: thesis:
then A2: EnsCatCoproductObj A = Union (coprod A) by Def9;
A3: EnsCatCoproduct A = Coprod A by A1, Def11;

per cases ;

suppose A4: Union (coprod A) <> {} ; :: thesis:

then A5: EnsCatCoproductObj A <> {} by A1, Def9;
thus A6: EnsCatCoproduct A is feasible :: thesis:

proof

let i be set ; :: according to ALTCAT_6:def 3 :: thesis:
assume A7: i in I ; :: thesis:
then reconsider I = I as non empty set ;
reconsider i = i as Element of I by A7;
reconsider A = A as ObjectsFamily of I,(EnsCat E) ;
reconsider P = EnsCatCoproduct A as MorphismsFamily of A, EnsCatCoproductObj A ;
take A . i ; :: thesis:
A8: <^(A . i),(EnsCatCoproductObj A)^> = Funcs ((A . i),(EnsCatCoproductObj A)) by ALTCAT_1:def 14;
Funcs ((A . i),(EnsCatCoproductObj A)) <> {} by A5;
then P . i in <^(A . i),(EnsCatCoproductObj A)^> by A8;
hence ( A . i = A . i & (EnsCatCoproduct A) . i in <^(A . i),(EnsCatCoproductObj A)^> ) ; :: thesis:

end;

let X be Object of (EnsCat E); :: according to ALTCAT_6:def 5 :: thesis:
let F be MorphismsFamily of A,X; :: thesis:
assume A9: F is feasible ; :: thesis:
A10: <^(EnsCatCoproductObj A),X^> = Funcs ((EnsCatCoproductObj A),X) by ALTCAT_1:def 14;
defpred S₁[ object , object ] means ( $1 `2 in I & $1 `1 in A . ($1 `2) & $2 = (F . ($1 `2)) . ($1 `1) & ( for j being object st j in I & $1 = [($1 `1),j] holds
(F . j) . ($1 `1) = $2 ) );
A11: for b being object st b in EnsCatCoproductObj A holds
ex u being object st S₁[b,u]

proof

let b be object ; :: thesis:
assume b in EnsCatCoproductObj A ; :: thesis:
then consider Z being set such that
A12: b in Z and
A13: Z in rng (coprod A) by A2, TARSKI:def 4;
consider i being object such that
A14: i in dom (coprod A) and
A15: (coprod A) . i = Z by A13, FUNCT_1:def 3;
(coprod A) . i = coprod (i,A) by A14, MSAFREE:def 3;
then consider x being set such that
A16: x in A . i and
A17: b = [x,i] by A12, A14, A15, MSAFREE:def 2;
take (F . i) . x ; :: thesis:
thus ( b `2 in I & b `1 in A . (b `2) & (F . (b `2)) . (b `1) = (F . i) . x ) by A14, A16, A17; :: thesis:
let j be object ; :: thesis:
assume that
j in I and
A18: b = [(b `1),j] ; :: thesis:
thus (F . j) . (b `1) = (F . i) . x by A17, A18, XTUPLE_0:1; :: thesis:

end;

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

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng ff ; :: thesis:
then consider x being object such that
A22: x in dom ff and
A23: ff . x = y by FUNCT_1:def 3;
set i = x `2 ;
A24: x `2 in I by A19, A20, A22;
A25: x `1 in A . (x `2) by A19, A20, A22;
A26: ff . x = (F . (x `2)) . (x `1) by A19, A20, A22;
consider o1 being Object of (EnsCat E) such that
A27: o1 = A . (x `2) and
F . (x `2) is Morphism of o1,X by A24, Def1;
A28: <^o1,X^> = Funcs (o1,X) by ALTCAT_1:def 14;
then A29: X <> {} by A24, A25, A27, A9, Def4;
F . (x `2) is Function of o1,X by A9, A24, A27, A28, Def4, FUNCT_2:66;
hence y in X by A23, A25, A26, A27, A29, FUNCT_2:5; :: thesis:

end;

then reconsider ff = ff as Morphism of (EnsCatCoproductObj A),X by A10, A19, FUNCT_2:def 2;
take ff ; :: thesis:
thus A30: ff in <^(EnsCatCoproductObj A),X^> by A10, A21, A19, 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 si,(EnsCatCoproductObj A) st
( si = A . i & Pi = (EnsCatCoproduct A) . i & F . i = ff * Pi ) :: thesis:

proof

let i be set ; :: thesis:
assume A31: i in I ; :: thesis:
then reconsider I = I as non empty set ;
reconsider j = i as Element of I by A31;
reconsider A1 = A as ObjectsFamily of I,(EnsCat E) ;
reconsider P1 = EnsCatCoproduct A as MorphismsFamily of A1, EnsCatCoproductObj A ;
reconsider F1 = F as MorphismsFamily of A1,X ;
take A1 . j ; :: thesis:
take P1 . j ; :: thesis:
thus ( A1 . j = A . i & P1 . j = (EnsCatCoproduct A) . i ) ; :: thesis:
reconsider p = P1 . j as Function ;
A32: <^(A1 . j),(EnsCatCoproductObj A)^> = Funcs ((A1 . j),(EnsCatCoproductObj A)) by ALTCAT_1:def 14;
A33: <^(A1 . j),(EnsCatCoproductObj A)^> <> {} by A6, Def4;
A34: <^(A1 . j),X^> = Funcs ((A1 . j),X) by ALTCAT_1:def 14;
<^(A1 . j),X^> <> {} by A9, Def4;
then A35: ff * (P1 . j) = ff * p by A30, A33, ALTCAT_1:16;
A36: F1 . j in Funcs ((A1 . j),X) by A34, A9, Def4;
then A37: dom (F1 . j) = A1 . j by FUNCT_2:92;
A38: dom (ff * (P1 . j)) = A1 . j by A34, A36, FUNCT_2:92;
A39: dom (P1 . j) = A1 . j by A32, A33, FUNCT_2:92;

now :: thesis:

let x be object ; :: thesis:
assume A40: x in dom (F1 . j) ; :: thesis:
p is Function of (A1 . j),(EnsCatCoproductObj A) by A32, A6, Def4, FUNCT_2:66;
then A41: p . x in EnsCatCoproductObj A by A5, A37, A40, FUNCT_2:5;
set x1 = (p . x) `1 ;
ex C being Function of (A . j),(Union (coprod A)) st
( (EnsCatCoproduct A) . i = C & ( for x being object st x in A . i holds
C . x = [x,i] ) ) by A3, Def10;
then A42: p . x = [x,j] by A37, A40;
then ff . (p . x) = (F . j) . ((p . x) `1) by A41, A20;
hence (ff * p) . x = (F1 . j) . x by A42, A37, A40, A39, FUNCT_1:13; :: thesis:

end;

hence F . i = ff * (P1 . j) by A35, A38, A36, FUNCT_1:2, FUNCT_2:92; :: thesis:

end;

let f1 be Morphism of (EnsCatCoproductObj A),X; :: thesis:
assume A43: for i being set st i in I holds
ex si being Object of (EnsCat E) ex Pi being Morphism of si,(EnsCatCoproductObj A) st
( si = A . i & Pi = (EnsCatCoproduct A) . i & F . i = f1 * Pi ) ; :: thesis:

per cases ;

suppose X = {} ; :: thesis:

then ( f1 = {} & ff = {} ) by A5, A10, SUBSET_1:def 1;
hence ff = f1 ; :: thesis:

end;

suppose A44: X <> {} ; :: thesis:

f1 is Function of (EnsCatCoproductObj A),X by A10, A30, FUNCT_2:66;
then A45: dom f1 = EnsCatCoproductObj A by A44, FUNCT_2:def 1;

now :: thesis:

let x be object ; :: thesis:
assume A46: x in dom ff ; :: thesis:
set a = x `1 ;
set i = x `2 ;
A47: x `2 in I by A19, A20, A46;
then consider C being Function of (A . (x `2)),(Union (coprod A)) such that
A48: (EnsCatCoproduct A) . (x `2) = C and
A49: for x being object st x in A . (x `2) holds
C . x = [x,(x `2)] by A3, Def10;
consider si being Object of (EnsCat E), Pi being Morphism of si,(EnsCatCoproductObj A) such that
si = A . (x `2) and
A50: Pi = (EnsCatCoproduct A) . (x `2) and
A51: F . (x `2) = f1 * Pi by A43, A47;
A52: x `1 in A . (x `2) by A19, A20, A46;
then A53: x `1 in dom Pi by A48, A50, A4, FUNCT_2:def 1;
A54: <^si,(EnsCatCoproductObj A)^> = Funcs (si,(EnsCatCoproductObj A)) by ALTCAT_1:def 14;
<^si,X^> = Funcs (si,X) by ALTCAT_1:def 14;
then A55: f1 * Pi = f1 * Pi by A2, A4, A44, A54, A10, ALTCAT_1:16;
A56: ex y, z being object st x = [y,z] by A2, A19, A46, CARD_3:21;
C . (x `1) = [(x `1),(x `2)] by A49, A52;
hence f1 . x = (F . (x `2)) . (x `1) by A48, A50, A56, A51, A53, A55, FUNCT_1:13
.= ff . x by A19, A20, A46 ;
:: thesis:

end;

hence ff = f1 by A19, A45, FUNCT_1:2; :: thesis:

end;

suppose A57: Union (coprod A) = {} ; :: thesis:

thus EnsCatCoproduct A is feasible :: thesis:

proof

let i be set ; :: according to ALTCAT_6:def 3 :: thesis:
assume A58: i in I ; :: thesis:
reconsider I = I as non empty set by A58;
reconsider i = i as Element of I by A58;
reconsider A = A as ObjectsFamily of I,(EnsCat E) ;
take A . i ; :: thesis:
A59: Coprod A is empty-yielding by A57, Th7;
A is empty-yielding by A57, Th8;
then A60: A . i = {} ;
A61: <^(A . i),(EnsCatCoproductObj A)^> = {{}} by A2, A57, A60, Lm2, ALTCAT_1:def 14;
(EnsCatCoproduct A) . i = {} by A3, A59;
hence ( A . i = A . i & (EnsCatCoproduct A) . i in <^(A . i),(EnsCatCoproductObj A)^> ) by A61, TARSKI:def 1; :: thesis:

end;

let X be Object of (EnsCat E); :: according to ALTCAT_6:def 5 :: thesis:
let F be MorphismsFamily of A,X; :: thesis:
assume F is feasible ; :: thesis:
A62: <^(EnsCatCoproductObj A),X^> = Funcs ((EnsCatCoproductObj A),X) by ALTCAT_1:def 14
.= {{}} by A2, A57, FUNCT_5:57 ;
then reconsider f = {} as Morphism of (EnsCatCoproductObj A),X by TARSKI:def 1;
take f ; :: thesis:
thus f in <^(EnsCatCoproductObj A),X^> by A62; :: thesis:
thus for i being set st i in I holds
ex si being Object of (EnsCat E) ex Pi being Morphism of si,(EnsCatCoproductObj A) st
( si = A . i & Pi = (EnsCatCoproduct A) . i & F . i = f * Pi ) :: thesis:

proof

let i be set ; :: thesis:
assume A63: i in I ; :: thesis:
reconsider J = I as non empty set by A63;
reconsider j = i as Element of J by A63;
reconsider A1 = A as ObjectsFamily of J,(EnsCat E) ;
reconsider P1 = EnsCatCoproduct A as MorphismsFamily of A1, EnsCatCoproductObj A ;
reconsider si = A1 . j as Object of (EnsCat E) ;
reconsider Pi = P1 . j as Morphism of si,(EnsCatCoproductObj A) ;
reconsider F1 = F as MorphismsFamily of A1,X ;
reconsider F2 = F1 . j as Morphism of si,X ;
take si ; :: thesis:
take Pi ; :: thesis:
thus ( si = A . i & Pi = (EnsCatCoproduct A) . i ) ; :: thesis:
A64: A is empty-yielding by A57, Th8;
then A65: si = {} ;
then A66: <^si,(EnsCatCoproductObj A)^> = {{}} by A2, A57, Lm2, ALTCAT_1:def 14;
A67: <^si,X^> <> {} by A62, A64, A2, A57;
A68: Funcs (si,X) = {{}} by A65, FUNCT_5:57;
A69: <^si,X^> = Funcs (si,X) by ALTCAT_1:def 14;
thus F . i = F2
.= {} by A68, A69, TARSKI:def 1
.= f * Pi
.= f * Pi by A62, A66, A67, ALTCAT_1:16 ; :: thesis:

end;

thus for f1 being Morphism of (EnsCatCoproductObj A),X st ( for i being set st i in I holds
ex si being Object of (EnsCat E) ex Pi being Morphism of si,(EnsCatCoproductObj A) st
( si = A . i & Pi = (EnsCatCoproduct A) . i & F . i = f1 * Pi ) ) holds
f = f1 by A62, TARSKI:def 1; :: thesis:

end;