let I be set ; :: thesis: for C being Category
for a, b being Object of C
for f being Morphism of C
for F being Injections_family of a,I st a is_a_coproduct_wrt F & dom f = a & cod f = b & f is invertible holds
b is_a_coproduct_wrt f * F
let C be Category; :: thesis: for a, b being Object of C
for f being Morphism of C
for F being Injections_family of a,I st a is_a_coproduct_wrt F & dom f = a & cod f = b & f is invertible holds
b is_a_coproduct_wrt f * F
let a, b be Object of C; :: thesis: for f being Morphism of C
for F being Injections_family of a,I st a is_a_coproduct_wrt F & dom f = a & cod f = b & f is invertible holds
b is_a_coproduct_wrt f * F
let f be Morphism of C; :: thesis: for F being Injections_family of a,I st a is_a_coproduct_wrt F & dom f = a & cod f = b & f is invertible holds
b is_a_coproduct_wrt f * F
let F be Injections_family of a,I; :: thesis: ( a is_a_coproduct_wrt F & dom f = a & cod f = b & f is invertible implies b is_a_coproduct_wrt f * F )
assume that
A1: a is_a_coproduct_wrt F and
A2: dom f = a and
A3: cod f = b and
A4: f is invertible ; :: thesis: b is_a_coproduct_wrt f * F
thus f * F is Injections_family of b,I by A2, A3, Th72; :: according to CAT_3:def 16 :: thesis: for d being Object of C
for F9 being Injections_family of d,I st doms (f * F) = doms F9 holds
ex h being Morphism of C st
( h in Hom (b,d) & ( for k being Morphism of C st k in Hom (b,d) holds
( ( for x being set st x in I holds
k * ((f * F) /. x) = F9 /. x ) iff h = k ) ) )
let c be Object of C; :: thesis: for F9 being Injections_family of c,I st doms (f * F) = doms F9 holds
ex h being Morphism of C st
( h in Hom (b,c) & ( for k being Morphism of C st k in Hom (b,c) holds
( ( for x being set st x in I holds
k * ((f * F) /. x) = F9 /. x ) iff h = k ) ) )
A5: cods F = I --> (dom f) by A2, Def17;
let F9 be Injections_family of c,I; :: thesis: ( doms (f * F) = doms F9 implies ex h being Morphism of C st
( h in Hom (b,c) & ( for k being Morphism of C st k in Hom (b,c) holds
( ( for x being set st x in I holds
k * ((f * F) /. x) = F9 /. x ) iff h = k ) ) ) )
assume doms (f * F) = doms F9 ; :: thesis: ex h being Morphism of C st
( h in Hom (b,c) & ( for k being Morphism of C st k in Hom (b,c) holds
( ( for x being set st x in I holds
k * ((f * F) /. x) = F9 /. x ) iff h = k ) ) )
then doms F = doms F9 by A5, Th21;
then consider h being Morphism of C such that
A6: h in Hom (a,c) and
A7: for k being Morphism of C st k in Hom (a,c) holds
( ( for x being set st x in I holds
k * (F /. x) = F9 /. x ) iff h = k ) by A1, Def18;
A8: dom h = a by A6, CAT_1:1;
consider g being Morphism of C such that
A9: dom g = cod f and
A10: cod g = dom f and
A11: f * g = id (cod f) and
A12: g * f = id (dom f) by A4, CAT_1:def 9;
cod h = c by A6, CAT_1:1;
then A13: cod (h * g) = c by A2, A10, A8, CAT_1:17;
take hg = h * g; :: thesis: ( hg in Hom (b,c) & ( for k being Morphism of C st k in Hom (b,c) holds
( ( for x being set st x in I holds
k * ((f * F) /. x) = F9 /. x ) iff hg = k ) ) )
dom (h * g) = b by A2, A3, A9, A10, A8, CAT_1:17;
hence hg in Hom (b,c) by A13; :: thesis: for k being Morphism of C st k in Hom (b,c) holds
( ( for x being set st x in I holds
k * ((f * F) /. x) = F9 /. x ) iff hg = k )
let k be Morphism of C; :: thesis: ( k in Hom (b,c) implies ( ( for x being set st x in I holds
k * ((f * F) /. x) = F9 /. x ) iff hg = k ) )
assume A14: k in Hom (b,c) ; :: thesis: ( ( for x being set st x in I holds
k * ((f * F) /. x) = F9 /. x ) iff hg = k )
then A15: dom k = b by CAT_1:1;
A16: cod k = c by A14, CAT_1:1;
thus ( ( for x being set st x in I holds
k * ((f * F) /. x) = F9 /. x ) implies hg = k ) :: thesis: ( hg = k implies for x being set st x in I holds
k * ((f * F) /. x) = F9 /. x )

proof

assume A17: for x being set st x in I holds
k * ((f * F) /. x) = F9 /. x ; :: thesis: hg = k

now

( cod (k * f) = c & dom (k * f) = a ) by A2, A3, A16, A15, CAT_1:17;
hence k * f in Hom (a,c) ; :: thesis: for x being set st x in I holds
(k * f) * (F /. x) = F9 /. x
let x be set ; :: thesis: ( x in I implies (k * f) * (F /. x) = F9 /. x )
assume A18: x in I ; :: thesis: (k * f) * (F /. x) = F9 /. x
then cod (F /. x) = a by Th67;
hence (k * f) * (F /. x) = k * (f * (F /. x)) by A2, A3, A15, CAT_1:18
.= k * ((f * F) /. x) by A18, Def8
.= F9 /. x by A17, A18 ;
:: thesis: verum

end;

then (k * f) * g = h * g by A7;
hence hg = k * (id b) by A3, A10, A11, A15, CAT_1:18
.= k by A15, CAT_1:22 ;
:: thesis: verum

end;

assume A19: hg = k ; :: thesis: for x being set st x in I holds
k * ((f * F) /. x) = F9 /. x
let x be set ; :: thesis: ( x in I implies k * ((f * F) /. x) = F9 /. x )
assume A20: x in I ; :: thesis: k * ((f * F) /. x) = F9 /. x
then A21: cod (F /. x) = a by Th67;
then A22: cod (f * (F /. x)) = b by A2, A3, CAT_1:17;
thus k * ((f * F) /. x) = k * (f * (F /. x)) by A20, Def8
.= h * (g * (f * (F /. x))) by A2, A3, A9, A10, A8, A19, A22, CAT_1:18
.= h * ((id (dom f)) * (F /. x)) by A2, A9, A12, A21, CAT_1:18
.= h * (F /. x) by A2, A21, CAT_1:21
.= F9 /. x by A6, A7, A20 ; :: thesis: verum