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 17 :: thesis: verum