let y be set ; :: thesis: for C being Category

for a being Object of C holds a is_a_coproduct_wrt y .--> (id a)

let C be Category; :: thesis: for a being Object of C holds a is_a_coproduct_wrt y .--> (id a)

let a be Object of C; :: thesis: a is_a_coproduct_wrt y .--> (id a)

set F = y .--> (id a);

cod (id a) = a ;

hence y .--> (id a) is Injections_family of a,{y} by Th64; :: according to CAT_3:def 17 :: thesis: for d being Object of C

for F9 being Injections_family of d,{y} st doms (y .--> (id a)) = doms F9 holds

ex h being Morphism of C st

( h in Hom (a,d) & ( for k being Morphism of C st k in Hom (a,d) holds

( ( for x being set st x in {y} holds

k (*) ((y .--> (id a)) /. x) = F9 /. x ) iff h = k ) ) )

let b be Object of C; :: thesis: for F9 being Injections_family of b,{y} st doms (y .--> (id a)) = doms F9 holds

ex h being Morphism of C st

( h in Hom (a,b) & ( for k being Morphism of C st k in Hom (a,b) holds

( ( for x being set st x in {y} holds

k (*) ((y .--> (id a)) /. x) = F9 /. x ) iff h = k ) ) )

let F9 be Injections_family of b,{y}; :: thesis: ( doms (y .--> (id a)) = doms F9 implies ex h being Morphism of C st

( h in Hom (a,b) & ( for k being Morphism of C st k in Hom (a,b) holds

( ( for x being set st x in {y} holds

k (*) ((y .--> (id a)) /. x) = F9 /. x ) iff h = k ) ) ) )

assume A1: doms (y .--> (id a)) = doms F9 ; :: thesis: ex h being Morphism of C st

( h in Hom (a,b) & ( for k being Morphism of C st k in Hom (a,b) holds

( ( for x being set st x in {y} holds

k (*) ((y .--> (id a)) /. x) = F9 /. x ) iff h = k ) ) )

take h = F9 /. y; :: thesis: ( h in Hom (a,b) & ( for k being Morphism of C st k in Hom (a,b) holds

( ( for x being set st x in {y} holds

k (*) ((y .--> (id a)) /. x) = F9 /. x ) iff h = k ) ) )

A2: y in {y} by TARSKI:def 1;

then A3: cod h = b by Th62;

dom h = (doms (y .--> (id a))) /. y by A1, A2, Def1

.= dom ((y .--> (id a)) /. y) by A2, Def1

.= dom (id a) by A2, Th2

.= a ;

hence h in Hom (a,b) by A3; :: thesis: for k being Morphism of C st k in Hom (a,b) holds

( ( for x being set st x in {y} holds

k (*) ((y .--> (id a)) /. x) = F9 /. x ) iff h = k )

let k be Morphism of C; :: thesis: ( k in Hom (a,b) implies ( ( for x being set st x in {y} holds

k (*) ((y .--> (id a)) /. x) = F9 /. x ) iff h = k ) )

assume k in Hom (a,b) ; :: thesis: ( ( for x being set st x in {y} holds

k (*) ((y .--> (id a)) /. x) = F9 /. x ) iff h = k )

then A4: dom k = a by CAT_1:1;

thus ( ( for x being set st x in {y} holds

k (*) ((y .--> (id a)) /. x) = F9 /. x ) implies h = k ) :: thesis: ( h = k implies for x being set st x in {y} holds

k (*) ((y .--> (id a)) /. x) = F9 /. x )

k (*) ((y .--> (id a)) /. x) = F9 /. x

let x be set ; :: thesis: ( x in {y} implies k (*) ((y .--> (id a)) /. x) = F9 /. x )

assume A7: x in {y} ; :: thesis: k (*) ((y .--> (id a)) /. x) = F9 /. x

hence F9 /. x = k by A6, TARSKI:def 1

.= k (*) (id a) by A4, CAT_1:22

.= k (*) ((y .--> (id a)) /. x) by A7, Th2 ;

:: thesis: verum

for a being Object of C holds a is_a_coproduct_wrt y .--> (id a)

let C be Category; :: thesis: for a being Object of C holds a is_a_coproduct_wrt y .--> (id a)

let a be Object of C; :: thesis: a is_a_coproduct_wrt y .--> (id a)

set F = y .--> (id a);

cod (id a) = a ;

hence y .--> (id a) is Injections_family of a,{y} by Th64; :: according to CAT_3:def 17 :: thesis: for d being Object of C

for F9 being Injections_family of d,{y} st doms (y .--> (id a)) = doms F9 holds

ex h being Morphism of C st

( h in Hom (a,d) & ( for k being Morphism of C st k in Hom (a,d) holds

( ( for x being set st x in {y} holds

k (*) ((y .--> (id a)) /. x) = F9 /. x ) iff h = k ) ) )

let b be Object of C; :: thesis: for F9 being Injections_family of b,{y} st doms (y .--> (id a)) = doms F9 holds

ex h being Morphism of C st

( h in Hom (a,b) & ( for k being Morphism of C st k in Hom (a,b) holds

( ( for x being set st x in {y} holds

k (*) ((y .--> (id a)) /. x) = F9 /. x ) iff h = k ) ) )

let F9 be Injections_family of b,{y}; :: thesis: ( doms (y .--> (id a)) = doms F9 implies ex h being Morphism of C st

( h in Hom (a,b) & ( for k being Morphism of C st k in Hom (a,b) holds

( ( for x being set st x in {y} holds

k (*) ((y .--> (id a)) /. x) = F9 /. x ) iff h = k ) ) ) )

assume A1: doms (y .--> (id a)) = doms F9 ; :: thesis: ex h being Morphism of C st

( h in Hom (a,b) & ( for k being Morphism of C st k in Hom (a,b) holds

( ( for x being set st x in {y} holds

k (*) ((y .--> (id a)) /. x) = F9 /. x ) iff h = k ) ) )

take h = F9 /. y; :: thesis: ( h in Hom (a,b) & ( for k being Morphism of C st k in Hom (a,b) holds

( ( for x being set st x in {y} holds

k (*) ((y .--> (id a)) /. x) = F9 /. x ) iff h = k ) ) )

A2: y in {y} by TARSKI:def 1;

then A3: cod h = b by Th62;

dom h = (doms (y .--> (id a))) /. y by A1, A2, Def1

.= dom ((y .--> (id a)) /. y) by A2, Def1

.= dom (id a) by A2, Th2

.= a ;

hence h in Hom (a,b) by A3; :: thesis: for k being Morphism of C st k in Hom (a,b) holds

( ( for x being set st x in {y} holds

k (*) ((y .--> (id a)) /. x) = F9 /. x ) iff h = k )

let k be Morphism of C; :: thesis: ( k in Hom (a,b) implies ( ( for x being set st x in {y} holds

k (*) ((y .--> (id a)) /. x) = F9 /. x ) iff h = k ) )

assume k in Hom (a,b) ; :: thesis: ( ( for x being set st x in {y} holds

k (*) ((y .--> (id a)) /. x) = F9 /. x ) iff h = k )

then A4: dom k = a by CAT_1:1;

thus ( ( for x being set st x in {y} holds

k (*) ((y .--> (id a)) /. x) = F9 /. x ) implies h = k ) :: thesis: ( h = k implies for x being set st x in {y} holds

k (*) ((y .--> (id a)) /. x) = F9 /. x )

proof

assume A6:
h = k
; :: thesis: for x being set st x in {y} holds
assume A5:
for x being set st x in {y} holds

k (*) ((y .--> (id a)) /. x) = F9 /. x ; :: thesis: h = k

thus k = k (*) (id a) by A4, CAT_1:22

.= k (*) ((y .--> (id a)) /. y) by A2, Th2

.= h by A2, A5 ; :: thesis: verum

end;k (*) ((y .--> (id a)) /. x) = F9 /. x ; :: thesis: h = k

thus k = k (*) (id a) by A4, CAT_1:22

.= k (*) ((y .--> (id a)) /. y) by A2, Th2

.= h by A2, A5 ; :: thesis: verum

k (*) ((y .--> (id a)) /. x) = F9 /. x

let x be set ; :: thesis: ( x in {y} implies k (*) ((y .--> (id a)) /. x) = F9 /. x )

assume A7: x in {y} ; :: thesis: k (*) ((y .--> (id a)) /. x) = F9 /. x

hence F9 /. x = k by A6, TARSKI:def 1

.= k (*) (id a) by A4, CAT_1:22

.= k (*) ((y .--> (id a)) /. x) by A7, Th2 ;

:: thesis: verum