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 Def17;
hence cods (f * F) = I --> (cod f) by Th21; :: according to CAT_3:def 15 :: thesis: verum