let B be Object of C; ( B is A -CatCoproduct-like implies B is initial )
assume A1:
B is A -CatCoproduct-like
; B is initial
for X being Object of C ex M being Morphism of B,X st
( M in <^B,X^> & ( for M1 being Morphism of B,X st M1 in <^B,X^> holds
M = M1 ) )
proof
let X be
Object of
C;
ex M being Morphism of B,X st
( M in <^B,X^> & ( for M1 being Morphism of B,X st M1 in <^B,X^> holds
M = M1 ) )
consider P being
MorphismsFamily of
A,
B such that A2:
(
P is
feasible &
P is
coprojection-morphisms )
by A1;
set F = the
MorphismsFamily of
A,
X;
consider f being
Morphism of
B,
X such that A3:
f in <^B,X^>
and
for
i being
set st
i in {} holds
ex
si being
Object of
C ex
Pi being
Morphism of
si,
B st
(
si = A . i &
Pi = P . i & the
MorphismsFamily of
A,
X . i = f * Pi )
and A4:
for
f1 being
Morphism of
B,
X st ( for
i being
set st
i in {} holds
ex
si being
Object of
C ex
Pi being
Morphism of
si,
B st
(
si = A . i &
Pi = P . i & the
MorphismsFamily of
A,
X . i = f1 * Pi ) ) holds
f = f1
by A2;
take
f
;
( f in <^B,X^> & ( for M1 being Morphism of B,X st M1 in <^B,X^> holds
f = M1 ) )
thus
f in <^B,X^>
by A3;
for M1 being Morphism of B,X st M1 in <^B,X^> holds
f = M1
let M be
Morphism of
B,
X;
( M in <^B,X^> implies f = M )
for
i being
set st
i in {} holds
ex
si being
Object of
C ex
Pi being
Morphism of
si,
B st
(
si = A . i &
Pi = P . i & the
MorphismsFamily of
A,
X . i = M * Pi )
;
hence
(
M in <^B,X^> implies
f = M )
by A4;
verum
end;
hence
B is initial
by ALTCAT_3:25; verum