set P = Coprod A;
set B = EnsCatCoproductObj A;
A2: EnsCatCoproductObj A = Union (coprod A) by A1, Def9;
let i be object ; :: according to ALTCAT_6:def 1 :: thesis: ( i in I implies ex o1 being Object of (EnsCat E) st
( o1 = A . i & (Coprod A) . i is Morphism of o1,(EnsCatCoproductObj A) ) )
assume A3: i in I ; :: thesis: ex o1 being Object of (EnsCat E) st
( o1 = A . i & (Coprod A) . i is Morphism of o1,(EnsCatCoproductObj A) )
consider F being Function of (A . i),(Union (coprod A)) such that
A4: (Coprod A) . i = F and
for x being object st x in A . i holds
F . x = [x,i] by A3, Def10;
reconsider J = I as non empty set by A3;
reconsider j = i as Element of J by A3;
reconsider A1 = A as ObjectsFamily of J,(EnsCat E) ;
A5: <^(A1 . j),(EnsCatCoproductObj A)^> = Funcs ((A1 . j),(EnsCatCoproductObj A)) by ALTCAT_1:def 14;
take o1 = A1 . j; :: thesis: ( o1 = A . i & (Coprod A) . i is Morphism of o1,(EnsCatCoproductObj A) )
thus o1 = A . i ; :: thesis: (Coprod A) . i is Morphism of o1,(EnsCatCoproductObj A)

per cases ( EnsCatCoproductObj A <> {} or EnsCatCoproductObj A = {} ) ;

suppose EnsCatCoproductObj A <> {} ; :: thesis: (Coprod A) . i is Morphism of o1,(EnsCatCoproductObj A)

hence (Coprod A) . i is Morphism of o1,(EnsCatCoproductObj A) by A2, A4, A5, FUNCT_2:8; :: thesis: verum

end;

suppose A6: EnsCatCoproductObj A = {} ; :: thesis: (Coprod A) . i is Morphism of o1,(EnsCatCoproductObj A)

then A7: (Coprod A) . i = {} by A4, A2;
dom (coprod A) = I by PARTFUN1:def 2;
then A8: (coprod A) . i in rng (coprod A) by A3, FUNCT_1:3;
( rng (coprod A) = {} or rng (coprod A) = {{}} ) by A2, A6, SCMYCIEL:18;
then (coprod A) . i = {} by A8, TARSKI:def 1;
then A . i = {} by A3, MSAFREE:2;
hence (Coprod A) . i is Morphism of o1,(EnsCatCoproductObj A) by A5, A7, A6, TARSKI:def 1, FUNCT_2:127; :: thesis: verum

end;

end;