let A, B be category; :: thesis: for C being non empty subcategory of A
for F being contravariant Functor of A,B
for a, b being Object of A
for c, d being Object of C st c = a & d = b & <^c,d^> <> {} holds
for f being Morphism of a,b
for g being Morphism of c,d st g = f holds
(F | C) . g = F . f
let C be non empty subcategory of A; :: thesis: for F being contravariant Functor of A,B
for a, b being Object of A
for c, d being Object of C st c = a & d = b & <^c,d^> <> {} holds
for f being Morphism of a,b
for g being Morphism of c,d st g = f holds
(F | C) . g = F . f
let F be contravariant Functor of A,B; :: thesis: for a, b being Object of A
for c, d being Object of C st c = a & d = b & <^c,d^> <> {} holds
for f being Morphism of a,b
for g being Morphism of c,d st g = f holds
(F | C) . g = F . f
let a, b be Object of A; :: thesis: for c, d being Object of C st c = a & d = b & <^c,d^> <> {} holds
for f being Morphism of a,b
for g being Morphism of c,d st g = f holds
(F | C) . g = F . f
let c, d be Object of C; :: thesis: ( c = a & d = b & <^c,d^> <> {} implies for f being Morphism of a,b
for g being Morphism of c,d st g = f holds
(F | C) . g = F . f )
assume that
A1: ( c = a & d = b ) and
A2: <^c,d^> <> {} ; :: thesis: for f being Morphism of a,b
for g being Morphism of c,d st g = f holds
(F | C) . g = F . f
let f be Morphism of a,b; :: thesis: for g being Morphism of c,d st g = f holds
(F | C) . g = F . f
let g be Morphism of c,d; :: thesis: ( g = f implies (F | C) . g = F . f )
assume g = f ; :: thesis: (F | C) . g = F . f
then A3: (incl C) . g = f by A2, Th27;
( (incl C) . c = a & (incl C) . d = b ) by A1, FUNCTOR0:27;
hence (F | C) . g = F . f by A2, A3, FUNCTOR3:8; :: thesis: verum