let A, B be category; :: thesis: for C being non empty subcategory of A
for F being FunctorStr of 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 of 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 of 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:28;
hence (F | C) . a = F . b by FUNCTOR0:34; :: thesis: verum