let y be set ; :: thesis: for C being Category
for a being Object of holds a is_a_coproduct_wrt y .--> (id a)
let C be Category; :: thesis: for a being Object of holds a is_a_coproduct_wrt y .--> (id a)
let a be Object of ; :: thesis: a is_a_coproduct_wrt y .--> (id a)
set F = y .--> (id a);
cod (id a) = a by CAT_1:44;
hence y .--> (id a) is Injections_family of a,{y} by Th69; :: according to CAT_3:def 18 :: thesis: for d being Object of
for F' being Injections_family of d,{y} st doms (y .--> (id a)) = doms F' holds
ex h being Morphism of st
( h in Hom a,d & ( for k being Morphism of st k in Hom a,d holds
( ( for x being set st x in {y} holds
k * ((y .--> (id a)) /. x) = F' /. x ) iff h = k ) ) )
let b be Object of ; :: thesis: for F' being Injections_family of b,{y} st doms (y .--> (id a)) = doms F' holds
ex h being Morphism of st
( h in Hom a,b & ( for k being Morphism of st k in Hom a,b holds
( ( for x being set st x in {y} holds
k * ((y .--> (id a)) /. x) = F' /. x ) iff h = k ) ) )
let F' be Injections_family of b,{y}; :: thesis: ( doms (y .--> (id a)) = doms F' implies ex h being Morphism of st
( h in Hom a,b & ( for k being Morphism of st k in Hom a,b holds
( ( for x being set st x in {y} holds
k * ((y .--> (id a)) /. x) = F' /. x ) iff h = k ) ) ) )
assume A1: doms (y .--> (id a)) = doms F' ; :: thesis: ex h being Morphism of st
( h in Hom a,b & ( for k being Morphism of st k in Hom a,b holds
( ( for x being set st x in {y} holds
k * ((y .--> (id a)) /. x) = F' /. x ) iff h = k ) ) )
take h = F' /. y; :: thesis: ( h in Hom a,b & ( for k being Morphism of st k in Hom a,b holds
( ( for x being set st x in {y} holds
k * ((y .--> (id a)) /. x) = F' /. x ) iff h = k ) ) )
A2: y in {y} by TARSKI:def 1;
then A3: cod h = b by Th67;
dom h = (doms (y .--> (id a))) /. y by A1, A2, Def3
.= dom ((y .--> (id a)) /. y) by A2, Def3
.= dom (id a) by A2, Th2
.= a by CAT_1:44 ;
hence h in Hom a,b by A3; :: thesis: for k being Morphism of st k in Hom a,b holds
( ( for x being set st x in {y} holds
k * ((y .--> (id a)) /. x) = F' /. x ) iff h = k )
let k be Morphism of ; :: thesis: ( k in Hom a,b implies ( ( for x being set st x in {y} holds
k * ((y .--> (id a)) /. x) = F' /. 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) = F' /. x ) iff h = k )
then A4: dom k = a by CAT_1:18;
thus ( ( for x being set st x in {y} holds
k * ((y .--> (id a)) /. x) = F' /. x ) implies h = k ) :: thesis: ( h = k implies for x being set st x in {y} holds
k * ((y .--> (id a)) /. x) = F' /. x )

proof

assume A5: for x being set st x in {y} holds
k * ((y .--> (id a)) /. x) = F' /. x ; :: thesis: h = k
thus k = k * (id a) by A4, CAT_1:47
.= k * ((y .--> (id a)) /. y) by A2, Th2
.= h by A2, A5 ; :: thesis: verum

end;

assume A6: h = k ; :: thesis: for x being set st x in {y} holds
k * ((y .--> (id a)) /. x) = F' /. x
let x be set ; :: thesis: ( x in {y} implies k * ((y .--> (id a)) /. x) = F' /. x )
assume A7: x in {y} ; :: thesis: k * ((y .--> (id a)) /. x) = F' /. x
hence F' /. x = k by A6, TARSKI:def 1
.= k * (id a) by A4, CAT_1:47
.= k * ((y .--> (id a)) /. x) by A7, Th2 ;
:: thesis: verum