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