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}

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

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