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 Def14;
hence doms (F * f) = I --> (dom f) by Th20; :: according to CAT_3:def 12 :: thesis: verum