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

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