let A, B be category; :: thesis: for C being non empty subcategory of non empty
for F being FunctorStr of A,B
for a being object of
for c being object of st c = a holds
(F | C) . c = F . a
let C be non empty subcategory of non empty ; :: thesis: for F being FunctorStr of A,B
for a being object of
for c being object of st c = a holds
(F | C) . c = F . a
let F be FunctorStr of A,B; :: thesis: for a being object of
for c being object of st c = a holds
(F | C) . c = F . a
let b be object of ; :: thesis: for c being object of st c = b holds
(F | C) . c = F . b
let a be object of ; :: 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