let I be set ; :: thesis: for C being Category
for a, b being Object of C
for f being Morphism of a,b
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 a,b
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 a,b
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 a,b; :: 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, Th66; :: according to CAT_3:def 17 :: 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, Def16;
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, Th17;
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;
A8: dom h = a by A6, CAT_1:1;
consider g being Morphism of b,a such that
A9: f * g = id b and
A10: g * f = id a by A4;
A11: ( Hom (b,a) <> {} & Hom (a,b) <> {} ) by A4;
then A12: dom g = cod f by A3, CAT_1:5;
A13: cod g = dom f by A2, A11, CAT_1:5;
A14: f * g = f (*) g by A11, CAT_1:def 13;
A15: g * f = g (*) f by A11, CAT_1:def 13;
cod h = c by A6, CAT_1:1;
then A16: cod (h (*) g) = c by A2, A13, 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, A12, A13, A8, CAT_1:17;
hence hg in Hom (b,c) by A16; :: 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 A17: 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 A18: dom k = b by CAT_1:1;
A19: cod k = c by A17, 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 A20: for x being set st x in I holds
k (*) ((f * F) /. x) = F9 /. x ; :: thesis: hg = k

now :: thesis: ( k (*) f in Hom (a,c) & ( for x being set st x in I holds
(k (*) f) (*) (F /. x) = F9 /. x ) )

( cod (k (*) f) = c & dom (k (*) f) = a ) by A2, A3, A19, A18, 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 A21: x in I ; :: thesis: (k (*) f) (*) (F /. x) = F9 /. x
then cod (F /. x) = a by Th62;
hence (k (*) f) (*) (F /. x) = k (*) (f (*) (F /. x)) by A2, A3, A18, CAT_1:18
.= k (*) ((f * F) /. x) by A21, Def6
.= F9 /. x by A20, A21 ;
:: thesis: verum

end;

then (k (*) f) (*) g = h (*) g by A7;
hence hg = k (*) (id b) by A3, A13, A9, A18, A14, CAT_1:18
.= k by A18, CAT_1:22 ;
:: thesis: verum

end;

assume A22: 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 A23: x in I ; :: thesis: k (*) ((f * F) /. x) = F9 /. x
then A24: cod (F /. x) = a by Th62;
then A25: cod (f (*) (F /. x)) = b by A2, A3, CAT_1:17;
thus k (*) ((f * F) /. x) = k (*) (f (*) (F /. x)) by A23, Def6
.= h (*) (g (*) (f (*) (F /. x))) by A2, A3, A12, A13, A8, A22, A25, CAT_1:18
.= h (*) ((id (dom f)) (*) (F /. x)) by A2, A12, A10, A24, A15, CAT_1:18
.= h (*) (F /. x) by A2, A24, CAT_1:21
.= F9 /. x by A6, A7, A23 ; :: thesis: verum