let A, B be category; for F1, F2 being covariant Functor of A,B
for e being natural_equivalence of F1,F2
for o being Object of A st F1,F2 are_naturally_equivalent holds
(e ") ! o = (e ! o) "
let F1, F2 be covariant Functor of A,B; for e being natural_equivalence of F1,F2
for o being Object of A st F1,F2 are_naturally_equivalent holds
(e ") ! o = (e ! o) "
let e be natural_equivalence of F1,F2; for o being Object of A st F1,F2 are_naturally_equivalent holds
(e ") ! o = (e ! o) "
let o be Object of A; ( F1,F2 are_naturally_equivalent implies (e ") ! o = (e ! o) " )
assume A1:
F1,F2 are_naturally_equivalent
; (e ") ! o = (e ! o) "
then
F2 is_transformable_to F1
;
hence (e ") ! o =
(e ") . o
by FUNCTOR2:def 4
.=
(e ! o) "
by A1, Def6
;
verum