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

for a being Object of C

for F being Function of I, the carrier' of C

for G being Projections_family of a,I st doms F = cods G holds

F "*" G is Projections_family of a,I

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

for F being Function of I, the carrier' of C

for G being Projections_family of a,I st doms F = cods G holds

F "*" G is Projections_family of a,I

let a be Object of C; :: thesis: for F being Function of I, the carrier' of C

for G being Projections_family of a,I st doms F = cods G holds

F "*" G is Projections_family of a,I

let F be Function of I, the carrier' of C; :: thesis: for G being Projections_family of a,I st doms F = cods G holds

F "*" G is Projections_family of a,I

let G be Projections_family of a,I; :: thesis: ( doms F = cods G implies F "*" G is Projections_family of a,I )

assume doms F = cods G ; :: thesis: F "*" G is Projections_family of a,I

then doms (F "*" G) = doms G by Th18;

hence doms (F "*" G) = I --> a by Def13; :: according to CAT_3:def 13 :: thesis: verum

for a being Object of C

for F being Function of I, the carrier' of C

for G being Projections_family of a,I st doms F = cods G holds

F "*" G is Projections_family of a,I

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

for F being Function of I, the carrier' of C

for G being Projections_family of a,I st doms F = cods G holds

F "*" G is Projections_family of a,I

let a be Object of C; :: thesis: for F being Function of I, the carrier' of C

for G being Projections_family of a,I st doms F = cods G holds

F "*" G is Projections_family of a,I

let F be Function of I, the carrier' of C; :: thesis: for G being Projections_family of a,I st doms F = cods G holds

F "*" G is Projections_family of a,I

let G be Projections_family of a,I; :: thesis: ( doms F = cods G implies F "*" G is Projections_family of a,I )

assume doms F = cods G ; :: thesis: F "*" G is Projections_family of a,I

then doms (F "*" G) = doms G by Th18;

hence doms (F "*" G) = I --> a by Def13; :: according to CAT_3:def 13 :: thesis: verum