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

for F being Function of {}, the carrier' of C holds F is Projections_family of a, {}

let a be Object of C; :: thesis: for F being Function of {}, the carrier' of C holds F is Projections_family of a, {}

let F be Function of {}, the carrier' of C; :: thesis: F is Projections_family of a, {}

thus {} --> a = doms F ; :: according to CAT_3:def 13 :: thesis: verum

for F being Function of {}, the carrier' of C holds F is Projections_family of a, {}

let a be Object of C; :: thesis: for F being Function of {}, the carrier' of C holds F is Projections_family of a, {}

let F be Function of {}, the carrier' of C; :: thesis: F is Projections_family of a, {}

thus {} --> a = doms F ; :: according to CAT_3:def 13 :: thesis: verum