let B, A 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 by Def4;
hence (e " ) ! o = (e " ) . o by FUNCTOR2:def 4
.= (e ! o) " by A1, Def6 ;
:: thesis: verum