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 )

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

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 A22:
hg = k
; :: thesis: for x being set st x in I holds
assume A20:
for x being set st x in I holds

k (*) ((f * F) /. x) = F9 /. x ; :: thesis: hg = k

hence hg = k (*) (id b) by A3, A13, A9, A18, A14, CAT_1:18

.= k by A18, CAT_1:22 ;

:: thesis: verum

end;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 ) )

then
(k (*) f) (*) g = h (*) g
by A7;(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;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

hence hg = k (*) (id b) by A3, A13, A9, A18, A14, CAT_1:18

.= k by A18, CAT_1:22 ;

:: thesis: verum

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