let y be set ; :: thesis: for C being Category
for a being Object of C
for f being Morphism of C st cod f = a holds
y .--> f is Injections_family of a,{y}
let C be Category; :: thesis: for a being Object of C
for f being Morphism of C st cod f = a holds
y .--> f is Injections_family of a,{y}
let a be Object of C; :: thesis: for f being Morphism of C st cod f = a holds
y .--> f is Injections_family of a,{y}
let f be Morphism of C; :: thesis: ( cod f = a implies y .--> f is Injections_family of a,{y} )
set F = y .--> f;
assume A1: cod f = a ; :: thesis: y .--> f is Injections_family of a,{y}

now :: thesis: for x being set st x in {y} holds
(cods (y .--> f)) /. x = (y .--> a) /. x

let x be set ; :: thesis: ( x in {y} implies (cods (y .--> f)) /. x = (y .--> a) /. x )
assume A2: x in {y} ; :: thesis: (cods (y .--> f)) /. x = (y .--> a) /. x
hence (cods (y .--> f)) /. x = cod ((y .--> f) /. x) by Def2
.= a by A1, A2, Th2
.= (y .--> a) /. x by A2, Th2 ;
:: thesis: verum

end;

hence cods (y .--> f) = {y} --> a by Th1; :: according to CAT_3:def 16 :: thesis: verum