let I be set ; :: thesis: for C being Category

for c, d being Object of C

for F being Injections_family of c,I

for F9 being Injections_family of d,I st c is_a_coproduct_wrt F & d is_a_coproduct_wrt F9 & doms F = doms F9 holds

c,d are_isomorphic

let C be Category; :: thesis: for c, d being Object of C

for F being Injections_family of c,I

for F9 being Injections_family of d,I st c is_a_coproduct_wrt F & d is_a_coproduct_wrt F9 & doms F = doms F9 holds

c,d are_isomorphic

let c, d be Object of C; :: thesis: for F being Injections_family of c,I

for F9 being Injections_family of d,I st c is_a_coproduct_wrt F & d is_a_coproduct_wrt F9 & doms F = doms F9 holds

c,d are_isomorphic

let F be Injections_family of c,I; :: thesis: for F9 being Injections_family of d,I st c is_a_coproduct_wrt F & d is_a_coproduct_wrt F9 & doms F = doms F9 holds

c,d are_isomorphic

let F9 be Injections_family of d,I; :: thesis: ( c is_a_coproduct_wrt F & d is_a_coproduct_wrt F9 & doms F = doms F9 implies c,d are_isomorphic )

assume that

A1: c is_a_coproduct_wrt F and

A2: d is_a_coproduct_wrt F9 and

A3: doms F = doms F9 ; :: thesis: c,d are_isomorphic

consider fg being Morphism of C such that

fg in Hom (d,d) and

A4: for k being Morphism of C st k in Hom (d,d) holds

( ( for x being set st x in I holds

k (*) (F9 /. x) = F9 /. x ) iff fg = k ) by A2;

consider f being Morphism of C such that

A5: f in Hom (c,d) and

A6: for k being Morphism of C st k in Hom (c,d) holds

( ( for x being set st x in I holds

k (*) (F /. x) = F9 /. x ) iff f = k ) by A1, A3;

reconsider f = f as Morphism of c,d by A5, CAT_1:def 5;

A7: dom f = c by A5, CAT_1:1;

gf in Hom (c,c) and

A10: for k being Morphism of C st k in Hom (c,c) holds

( ( for x being set st x in I holds

k (*) (F /. x) = F /. x ) iff gf = k ) by A1;

consider g being Morphism of C such that

A11: g in Hom (d,c) and

A12: for k being Morphism of C st k in Hom (d,c) holds

( ( for x being set st x in I holds

k (*) (F9 /. x) = F /. x ) iff g = k ) by A2, A3;

reconsider g = g as Morphism of d,c by A11, CAT_1:def 5;

take f ; :: according to CAT_1:def 20 :: thesis: f is invertible

thus ( Hom (c,d) <> {} & Hom (d,c) <> {} ) by A11, A5; :: according to CAT_1:def 16 :: thesis: ex b_{1} being Morphism of d,c st

( f * b_{1} = id d & b_{1} * f = id c )

take g ; :: thesis: ( f * g = id d & g * f = id c )

A13: cod f = d by A5, CAT_1:1;

A14: dom g = d by A11, CAT_1:1;

A15: cod g = c by A11, CAT_1:1;

.= fg by A4, A16

.= id d by A4, A9 ; :: thesis: g * f = id c

.= gf by A10, A18

.= id c by A8, A10 ; :: thesis: verum

for c, d being Object of C

for F being Injections_family of c,I

for F9 being Injections_family of d,I st c is_a_coproduct_wrt F & d is_a_coproduct_wrt F9 & doms F = doms F9 holds

c,d are_isomorphic

let C be Category; :: thesis: for c, d being Object of C

for F being Injections_family of c,I

for F9 being Injections_family of d,I st c is_a_coproduct_wrt F & d is_a_coproduct_wrt F9 & doms F = doms F9 holds

c,d are_isomorphic

let c, d be Object of C; :: thesis: for F being Injections_family of c,I

for F9 being Injections_family of d,I st c is_a_coproduct_wrt F & d is_a_coproduct_wrt F9 & doms F = doms F9 holds

c,d are_isomorphic

let F be Injections_family of c,I; :: thesis: for F9 being Injections_family of d,I st c is_a_coproduct_wrt F & d is_a_coproduct_wrt F9 & doms F = doms F9 holds

c,d are_isomorphic

let F9 be Injections_family of d,I; :: thesis: ( c is_a_coproduct_wrt F & d is_a_coproduct_wrt F9 & doms F = doms F9 implies c,d are_isomorphic )

assume that

A1: c is_a_coproduct_wrt F and

A2: d is_a_coproduct_wrt F9 and

A3: doms F = doms F9 ; :: thesis: c,d are_isomorphic

consider fg being Morphism of C such that

fg in Hom (d,d) and

A4: for k being Morphism of C st k in Hom (d,d) holds

( ( for x being set st x in I holds

k (*) (F9 /. x) = F9 /. x ) iff fg = k ) by A2;

consider f being Morphism of C such that

A5: f in Hom (c,d) and

A6: for k being Morphism of C st k in Hom (c,d) holds

( ( for x being set st x in I holds

k (*) (F /. x) = F9 /. x ) iff f = k ) by A1, A3;

reconsider f = f as Morphism of c,d by A5, CAT_1:def 5;

A7: dom f = c by A5, CAT_1:1;

A8: now :: thesis: ( id c in Hom (c,c) & ( for x being set st x in I holds

(id c) (*) (F /. x) = F /. x ) )

(id c) (*) (F /. x) = F /. x ) )

set k = id c;

thus id c in Hom (c,c) by CAT_1:27; :: thesis: for x being set st x in I holds

(id c) (*) (F /. x) = F /. x

let x be set ; :: thesis: ( x in I implies (id c) (*) (F /. x) = F /. x )

assume x in I ; :: thesis: (id c) (*) (F /. x) = F /. x

then cod (F /. x) = c by Th62;

hence (id c) (*) (F /. x) = F /. x by CAT_1:21; :: thesis: verum

end;thus id c in Hom (c,c) by CAT_1:27; :: thesis: for x being set st x in I holds

(id c) (*) (F /. x) = F /. x

let x be set ; :: thesis: ( x in I implies (id c) (*) (F /. x) = F /. x )

assume x in I ; :: thesis: (id c) (*) (F /. x) = F /. x

then cod (F /. x) = c by Th62;

hence (id c) (*) (F /. x) = F /. x by CAT_1:21; :: thesis: verum

A9: now :: thesis: ( id d in Hom (d,d) & ( for x being set st x in I holds

(id d) (*) (F9 /. x) = F9 /. x ) )

consider gf being Morphism of C such that (id d) (*) (F9 /. x) = F9 /. x ) )

set k = id d;

thus id d in Hom (d,d) by CAT_1:27; :: thesis: for x being set st x in I holds

(id d) (*) (F9 /. x) = F9 /. x

let x be set ; :: thesis: ( x in I implies (id d) (*) (F9 /. x) = F9 /. x )

assume x in I ; :: thesis: (id d) (*) (F9 /. x) = F9 /. x

then cod (F9 /. x) = d by Th62;

hence (id d) (*) (F9 /. x) = F9 /. x by CAT_1:21; :: thesis: verum

end;thus id d in Hom (d,d) by CAT_1:27; :: thesis: for x being set st x in I holds

(id d) (*) (F9 /. x) = F9 /. x

let x be set ; :: thesis: ( x in I implies (id d) (*) (F9 /. x) = F9 /. x )

assume x in I ; :: thesis: (id d) (*) (F9 /. x) = F9 /. x

then cod (F9 /. x) = d by Th62;

hence (id d) (*) (F9 /. x) = F9 /. x by CAT_1:21; :: thesis: verum

gf in Hom (c,c) and

A10: for k being Morphism of C st k in Hom (c,c) holds

( ( for x being set st x in I holds

k (*) (F /. x) = F /. x ) iff gf = k ) by A1;

consider g being Morphism of C such that

A11: g in Hom (d,c) and

A12: for k being Morphism of C st k in Hom (d,c) holds

( ( for x being set st x in I holds

k (*) (F9 /. x) = F /. x ) iff g = k ) by A2, A3;

reconsider g = g as Morphism of d,c by A11, CAT_1:def 5;

take f ; :: according to CAT_1:def 20 :: thesis: f is invertible

thus ( Hom (c,d) <> {} & Hom (d,c) <> {} ) by A11, A5; :: according to CAT_1:def 16 :: thesis: ex b

( f * b

take g ; :: thesis: ( f * g = id d & g * f = id c )

A13: cod f = d by A5, CAT_1:1;

A14: dom g = d by A11, CAT_1:1;

A15: cod g = c by A11, CAT_1:1;

A16: now :: thesis: ( f (*) g in Hom (d,d) & ( for x being set st x in I holds

(f (*) g) (*) (F9 /. x) = F9 /. x ) )

thus f * g =
f (*) g
by A11, A5, CAT_1:def 13
(f (*) g) (*) (F9 /. x) = F9 /. x ) )

( cod (f (*) g) = d & dom (f (*) g) = d )
by A13, A14, A7, A15, CAT_1:17;

hence f (*) g in Hom (d,d) ; :: thesis: for x being set st x in I holds

(f (*) g) (*) (F9 /. x) = F9 /. x

let x be set ; :: thesis: ( x in I implies (f (*) g) (*) (F9 /. x) = F9 /. x )

assume A17: x in I ; :: thesis: (f (*) g) (*) (F9 /. x) = F9 /. x

then cod (F9 /. x) = d by Th62;

hence (f (*) g) (*) (F9 /. x) = f (*) (g (*) (F9 /. x)) by A14, A7, A15, CAT_1:18

.= f (*) (F /. x) by A11, A12, A17

.= F9 /. x by A5, A6, A17 ;

:: thesis: verum

end;hence f (*) g in Hom (d,d) ; :: thesis: for x being set st x in I holds

(f (*) g) (*) (F9 /. x) = F9 /. x

let x be set ; :: thesis: ( x in I implies (f (*) g) (*) (F9 /. x) = F9 /. x )

assume A17: x in I ; :: thesis: (f (*) g) (*) (F9 /. x) = F9 /. x

then cod (F9 /. x) = d by Th62;

hence (f (*) g) (*) (F9 /. x) = f (*) (g (*) (F9 /. x)) by A14, A7, A15, CAT_1:18

.= f (*) (F /. x) by A11, A12, A17

.= F9 /. x by A5, A6, A17 ;

:: thesis: verum

.= fg by A4, A16

.= id d by A4, A9 ; :: thesis: g * f = id c

A18: now :: thesis: ( g (*) f in Hom (c,c) & ( for x being set st x in I holds

(g (*) f) (*) (F /. x) = F /. x ) )

thus g * f =
g (*) f
by A11, A5, CAT_1:def 13
(g (*) f) (*) (F /. x) = F /. x ) )

( cod (g (*) f) = c & dom (g (*) f) = c )
by A13, A14, A7, A15, CAT_1:17;

hence g (*) f in Hom (c,c) ; :: thesis: for x being set st x in I holds

(g (*) f) (*) (F /. x) = F /. x

let x be set ; :: thesis: ( x in I implies (g (*) f) (*) (F /. x) = F /. x )

assume A19: x in I ; :: thesis: (g (*) f) (*) (F /. x) = F /. x

then cod (F /. x) = c by Th62;

hence (g (*) f) (*) (F /. x) = g (*) (f (*) (F /. x)) by A13, A14, A7, CAT_1:18

.= g (*) (F9 /. x) by A5, A6, A19

.= F /. x by A11, A12, A19 ;

:: thesis: verum

end;hence g (*) f in Hom (c,c) ; :: thesis: for x being set st x in I holds

(g (*) f) (*) (F /. x) = F /. x

let x be set ; :: thesis: ( x in I implies (g (*) f) (*) (F /. x) = F /. x )

assume A19: x in I ; :: thesis: (g (*) f) (*) (F /. x) = F /. x

then cod (F /. x) = c by Th62;

hence (g (*) f) (*) (F /. x) = g (*) (f (*) (F /. x)) by A13, A14, A7, CAT_1:18

.= g (*) (F9 /. x) by A5, A6, A19

.= F /. x by A11, A12, A19 ;

:: thesis: verum

.= gf by A10, A18

.= id c by A8, A10 ; :: thesis: verum