let I, x be set ; :: thesis: for C being Category

for c being Object of C

for F being Injections_family of c,I st x in I holds

cod (F /. x) = c

let C be Category; :: thesis: for c being Object of C

for F being Injections_family of c,I st x in I holds

cod (F /. x) = c

let c be Object of C; :: thesis: for F being Injections_family of c,I st x in I holds

cod (F /. x) = c

let F be Injections_family of c,I; :: thesis: ( x in I implies cod (F /. x) = c )

assume A1: x in I ; :: thesis: cod (F /. x) = c

(cods F) /. x = (I --> c) /. x by Def16;

hence cod (F /. x) = (I --> c) /. x by A1, Def2

.= c by A1, Th2 ;

:: thesis: verum

for c being Object of C

for F being Injections_family of c,I st x in I holds

cod (F /. x) = c

let C be Category; :: thesis: for c being Object of C

for F being Injections_family of c,I st x in I holds

cod (F /. x) = c

let c be Object of C; :: thesis: for F being Injections_family of c,I st x in I holds

cod (F /. x) = c

let F be Injections_family of c,I; :: thesis: ( x in I implies cod (F /. x) = c )

assume A1: x in I ; :: thesis: cod (F /. x) = c

(cods F) /. x = (I --> c) /. x by Def16;

hence cod (F /. x) = (I --> c) /. x by A1, Def2

.= c by A1, Th2 ;

:: thesis: verum