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

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