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