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