let C be Category; :: thesis: for a being Object of C
for F being Function of {}, the carrier' of C holds F is Injections_family of a, {}
let a be Object of C; :: thesis: for F being Function of {}, the carrier' of C holds F is Injections_family of a, {}
let F be Function of {}, the carrier' of C; :: thesis: F is Injections_family of a, {}
thus {} --> a = cods F ; :: according to CAT_3:def 15 :: thesis: verum