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