let I be set ; :: thesis: for C being Category
for b being Object of C
for F being Injections_family of b,I
for G being Function of I, the carrier' of C st doms F = cods G holds
F "*" G is Injections_family of b,I
let C be Category; :: thesis: for b being Object of C
for F being Injections_family of b,I
for G being Function of I, the carrier' of C st doms F = cods G holds
F "*" G is Injections_family of b,I
let b be Object of C; :: thesis: for F being Injections_family of b,I
for G being Function of I, the carrier' of C st doms F = cods G holds
F "*" G is Injections_family of b,I
let F be Injections_family of b,I; :: thesis: for G being Function of I, the carrier' of C st doms F = cods G holds
F "*" G is Injections_family of b,I
let G be Function of I, the carrier' of C; :: thesis: ( doms F = cods G implies F "*" G is Injections_family of b,I )
assume doms F = cods G ; :: thesis: F "*" G is Injections_family of b,I
then cods (F "*" G) = cods F by Th18;
hence cods (F "*" G) = I --> b by Def16; :: according to CAT_3:def 16 :: thesis: verum