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

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