set P = Coprod A;
set B = EnsCatCoproductObj A;
A2:
EnsCatCoproductObj A = Union (coprod A)
by A1, Def9;
let i be object ; ALTCAT_6:def 1 ( 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
; 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; ( o1 = A . i & (Coprod A) . i is Morphism of o1,(EnsCatCoproductObj A) )
thus
o1 = A . i
; (Coprod A) . i is Morphism of o1,(EnsCatCoproductObj A)
per cases
( EnsCatCoproductObj A <> {} or EnsCatCoproductObj A = {} )
;
suppose A6:
EnsCatCoproductObj A = {}
;
(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;
verum end;