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

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