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 & cod f = b ) and
A3: f is invertible ; :: thesis: b is_a_coproduct_wrt f * F
thus f * F is Injections_family of b,I by A2, Th72; :: according to CAT_3:def 18 :: thesis: for d being Object of C
for F' being Injections_family of d,I st doms (f * F) = doms F' 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) = F' /. x ) iff h = k ) ) )
let c be Object of C; :: thesis: for F' being Injections_family of c,I st doms (f * F) = doms F' 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) = F' /. x ) iff h = k ) ) )
let F' be Injections_family of c,I; :: thesis: ( doms (f * F) = doms F' 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) = F' /. x ) iff h = k ) ) ) )
assume A4: doms (f * F) = doms F' ; :: 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) = F' /. x ) iff h = k ) ) )
cods F = I --> (dom f) by A2, Def17;
then doms F = doms F' by A4, Th21;
then consider h being Morphism of C such that
A5: h in Hom a,c and
A6: 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) = F' /. x ) iff h = k ) by A1, Def18;
consider g being Morphism of C such that
A7: ( dom g = cod f & cod g = dom f ) and
A8: f * g = id (cod f) and
A9: g * f = id (dom f) by A3, CAT_1:def 12;
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) = F' /. x ) iff hg = k ) ) )
A10: ( dom h = a & cod h = c ) by A5, CAT_1:18;
then ( cod (h * g) = c & dom (h * g) = b ) by A2, A7, CAT_1:42;
hence hg in Hom b,c ; :: 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) = F' /. 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) = F' /. x ) iff hg = k ) )
assume k in Hom b,c ; :: thesis: ( ( for x being set st x in I holds
k * ((f * F) /. x) = F' /. x ) iff hg = k )
then A11: ( cod k = c & dom k = b ) by CAT_1:18;
thus ( ( for x being set st x in I holds
k * ((f * F) /. x) = F' /. x ) implies hg = k ) :: thesis: ( hg = k implies for x being set st x in I holds
k * ((f * F) /. x) = F' /. x )

proof

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

now

( cod (k * f) = c & dom (k * f) = a ) by A2, A11, CAT_1:42;
hence k * f in Hom a,c ; :: thesis: for x being set st x in I holds
(k * f) * (F /. x) = F' /. x
let x be set ; :: thesis: ( x in I implies (k * f) * (F /. x) = F' /. x )
assume A13: x in I ; :: thesis: (k * f) * (F /. x) = F' /. x
then cod (F /. x) = a by Th67;
hence (k * f) * (F /. x) = k * (f * (F /. x)) by A2, A11, CAT_1:43
.= k * ((f * F) /. x) by A13, Def8
.= F' /. x by A12, A13 ;
:: thesis: verum

end;

then (k * f) * g = h * g by A6;
hence hg = k * (id b) by A2, A7, A8, A11, CAT_1:43
.= k by A11, CAT_1:47 ;
:: thesis: verum

end;

assume A14: hg = k ; :: thesis: for x being set st x in I holds
k * ((f * F) /. x) = F' /. x
let x be set ; :: thesis: ( x in I implies k * ((f * F) /. x) = F' /. x )
assume A15: x in I ; :: thesis: k * ((f * F) /. x) = F' /. x
then A16: cod (F /. x) = a by Th67;
then A17: cod (f * (F /. x)) = b by A2, CAT_1:42;
thus k * ((f * F) /. x) = k * (f * (F /. x)) by A15, Def8
.= h * (g * (f * (F /. x))) by A2, A7, A10, A14, A17, CAT_1:43
.= h * ((id (dom f)) * (F /. x)) by A2, A7, A9, A16, CAT_1:43
.= h * (F /. x) by A2, A16, CAT_1:46
.= F' /. x by A5, A6, A15 ; :: thesis: verum