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

for a being Object of C

for f being Morphism of C

for F being Projections_family of a,I st cod f = a holds

F * f is Projections_family of dom f,I

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

for f being Morphism of C

for F being Projections_family of a,I st cod f = a holds

F * f is Projections_family of dom f,I

let a be Object of C; :: thesis: for f being Morphism of C

for F being Projections_family of a,I st cod f = a holds

F * f is Projections_family of dom f,I

let f be Morphism of C; :: thesis: for F being Projections_family of a,I st cod f = a holds

F * f is Projections_family of dom f,I

let F be Projections_family of a,I; :: thesis: ( cod f = a implies F * f is Projections_family of dom f,I )

assume cod f = a ; :: thesis: F * f is Projections_family of dom f,I

then doms F = I --> (cod f) by Def13;

hence doms (F * f) = I --> (dom f) by Th16; :: according to CAT_3:def 13 :: thesis: verum

for a being Object of C

for f being Morphism of C

for F being Projections_family of a,I st cod f = a holds

F * f is Projections_family of dom f,I

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

for f being Morphism of C

for F being Projections_family of a,I st cod f = a holds

F * f is Projections_family of dom f,I

let a be Object of C; :: thesis: for f being Morphism of C

for F being Projections_family of a,I st cod f = a holds

F * f is Projections_family of dom f,I

let f be Morphism of C; :: thesis: for F being Projections_family of a,I st cod f = a holds

F * f is Projections_family of dom f,I

let F be Projections_family of a,I; :: thesis: ( cod f = a implies F * f is Projections_family of dom f,I )

assume cod f = a ; :: thesis: F * f is Projections_family of dom f,I

then doms F = I --> (cod f) by Def13;

hence doms (F * f) = I --> (dom f) by Th16; :: according to CAT_3:def 13 :: thesis: verum