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

for b being Object of C

for f being Morphism of C

for F being Injections_family of b,I st dom f = b holds

f * F is Injections_family of cod f,I

let C be Category; :: thesis: for b being Object of C

for f being Morphism of C

for F being Injections_family of b,I st dom f = b holds

f * F is Injections_family of cod f,I

let b be Object of C; :: thesis: for f being Morphism of C

for F being Injections_family of b,I st dom f = b holds

f * F is Injections_family of cod f,I

let f be Morphism of C; :: thesis: for F being Injections_family of b,I st dom f = b holds

f * F is Injections_family of cod f,I

let F be Injections_family of b,I; :: thesis: ( dom f = b implies f * F is Injections_family of cod f,I )

assume dom f = b ; :: thesis: f * F is Injections_family of cod f,I

then cods F = I --> (dom f) by Def16;

hence cods (f * F) = I --> (cod f) by Th17; :: according to CAT_3:def 16 :: thesis: verum

for b being Object of C

for f being Morphism of C

for F being Injections_family of b,I st dom f = b holds

f * F is Injections_family of cod f,I

let C be Category; :: thesis: for b being Object of C

for f being Morphism of C

for F being Injections_family of b,I st dom f = b holds

f * F is Injections_family of cod f,I

let b be Object of C; :: thesis: for f being Morphism of C

for F being Injections_family of b,I st dom f = b holds

f * F is Injections_family of cod f,I

let f be Morphism of C; :: thesis: for F being Injections_family of b,I st dom f = b holds

f * F is Injections_family of cod f,I

let F be Injections_family of b,I; :: thesis: ( dom f = b implies f * F is Injections_family of cod f,I )

assume dom f = b ; :: thesis: f * F is Injections_family of cod f,I

then cods F = I --> (dom f) by Def16;

hence cods (f * F) = I --> (cod f) by Th17; :: according to CAT_3:def 16 :: thesis: verum