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

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