let A, B be Category; :: thesis: for F being Functor of A,B
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds ((id F) . b) * (F /. f) = (F /. f) * ((id F) . a)
let F be Functor of A,B; :: thesis: for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds ((id F) . b) * (F /. f) = (F /. f) * ((id F) . a)
let a, b be Object of A; :: thesis: ( Hom (a,b) <> {} implies for f being Morphism of a,b holds ((id F) . b) * (F /. f) = (F /. f) * ((id F) . a) )
assume A1: Hom (a,b) <> {} ; :: thesis: for f being Morphism of a,b holds ((id F) . b) * (F /. f) = (F /. f) * ((id F) . a)
let f be Morphism of a,b; :: thesis: ((id F) . b) * (F /. f) = (F /. f) * ((id F) . a)
A2: Hom (a,a) <> {} ;
A3: Hom (b,b) <> {} ;
thus ((id F) . b) * (F /. f) = (id (F . b)) * (F /. f) by Th16
.= (F /. (id b)) * (F /. f) by Th11
.= F /. ((id b) * f) by A1, A3, Th9
.= F /. f by A1, CAT_1:28
.= F /. (f * (id a)) by A1, CAT_1:29
.= (F /. f) * (F /. (id a)) by A1, A2, Th9
.= (F /. f) * (id (F . a)) by Th11
.= (F /. f) * ((id F) . a) by Th16 ; :: thesis: verum