let I be set ; 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; 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; 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; 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; ( dom f = b implies f * F is Injections_family of cod f,I )
assume
dom f = b
; 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; CAT_3:def 16 verum