let C be category; :: thesis: for A being ObjectsFamily of {},C
for B being Object of C st B is initial holds
ex P being MorphismsFamily of A,B st
( P is empty & P is coprojection-morphisms )
let A be ObjectsFamily of {},C; :: thesis: for B being Object of C st B is initial holds
ex P being MorphismsFamily of A,B st
( P is empty & P is coprojection-morphisms )
let B be Object of C; :: thesis: ( B is initial implies ex P being MorphismsFamily of A,B st
( P is empty & P is coprojection-morphisms ) )
assume A1: B is initial ; :: thesis: ex P being MorphismsFamily of A,B st
( P is empty & P is coprojection-morphisms )
reconsider P = {} as MorphismsFamily of A,B by Th1;
take P ; :: thesis: ( P is empty & P is coprojection-morphisms )
thus P is empty ; :: thesis: P is coprojection-morphisms
let X be Object of C; :: according to ALTCAT_6:def 5 :: thesis: for F being MorphismsFamily of A,X st F is feasible holds
ex f being Morphism of B,X st
( f in <^B,X^> & ( 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 & F . i = f * Pi ) ) & ( 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 & F . i = f1 * Pi ) ) holds
f = f1 ) )
let F be MorphismsFamily of A,X; :: thesis: ( F is feasible implies ex f being Morphism of B,X st
( f in <^B,X^> & ( 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 & F . i = f * Pi ) ) & ( 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 & F . i = f1 * Pi ) ) holds
f = f1 ) ) )
assume F is feasible ; :: thesis: ex f being Morphism of B,X st
( f in <^B,X^> & ( 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 & F . i = f * Pi ) ) & ( 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 & F . i = f1 * Pi ) ) holds
f = f1 ) )
consider f being Morphism of B,X such that
A2: ( f in <^B,X^> & ( for M1 being Morphism of B,X st M1 in <^B,X^> holds
f = M1 ) ) by A1, ALTCAT_3:25;
take f ; :: thesis: ( f in <^B,X^> & ( 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 & F . i = f * Pi ) ) & ( 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 & F . i = f1 * Pi ) ) holds
f = f1 ) )
thus ( f in <^B,X^> & ( 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 & F . i = f * Pi ) ) & ( 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 & F . i = f1 * Pi ) ) holds
f = f1 ) ) by A2; :: thesis: verum