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