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:
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 ;
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 ;
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 ;
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 ;
A13: cod g = dom f by ;
A14: f * g = f (*) g by ;
A15: g * f = g (*) f by ;
cod h = c by ;
then A16: cod (h (*) g) = c by ;
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 ;
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 ;
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
.= k (*) ((f * F) /. x) by
.= F9 /. x by ;
:: thesis: verum
end;
then (k (*) f) (*) g = h (*) g by A7;
hence hg = k (*) (id b) by
.= k by ;
:: 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 ;
thus k (*) ((f * F) /. x) = k (*) (f (*) (F /. x)) by
.= h (*) (g (*) (f (*) (F /. x))) by A2, A3, A12, A13, A8, A22, A25, CAT_1:18
.= h (*) ((id (dom f)) (*) (F /. x)) by
.= h (*) (F /. x) by
.= F9 /. x by A6, A7, A23 ; :: thesis: verum