let A, B be category; :: thesis: 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; :: thesis: 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; :: thesis: for o being Object of A st F1,F2 are_naturally_equivalent holds
(e ") ! o = (e ! o) "
let o be Object of A; :: thesis: ( F1,F2 are_naturally_equivalent implies (e ") ! o = (e ! o) " )
assume A1: F1,F2 are_naturally_equivalent ; :: thesis: (e ") ! o = (e ! o) "
then F2 is_transformable_to F1 ;
hence (e ") ! o = (e ") . o by FUNCTOR2:def 4
.= (e ! o) " by A1, Def6 ;
:: thesis: verum