let A, B be category; :: thesis: for C being non empty subcategory of A
for F being FunctorStr over A,B
for a being Object of A
for c being Object of C st c = a holds
(F | C) . c = F . a
let C be non empty subcategory of A; :: thesis: for F being FunctorStr over A,B
for a being Object of A
for c being Object of C st c = a holds
(F | C) . c = F . a
let F be FunctorStr over A,B; :: thesis: for a being Object of A
for c being Object of C st c = a holds
(F | C) . c = F . a
let b be Object of A; :: thesis: for c being Object of C st c = b holds
(F | C) . c = F . b
let a be Object of C; :: thesis: ( a = b implies (F | C) . a = F . b )
assume a = b ; :: thesis: (F | C) . a = F . b
then (incl C) . a = b by FUNCTOR0:27;
hence (F | C) . a = F . b by FUNCTOR0:33; :: thesis: verum