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 )
proof
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;
assume A6: h = k ; :: thesis: for x being set st x in {y} holds
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