let C1, C2 be category; :: thesis: for F1, F2, T being Functor of C1,C2 st F1 is covariant & F2 is covariant holds
( T is_natural_transformation_of F1,F2 iff for f, f1, f2 being morphism of C1 st f1 is identity & f2 is identity & f1 |> f & f |> f2 holds
( T . f1 |> F1 . f & F2 . f |> T . f2 & T . f = (T . f1) (*) (F1 . f) & T . f = (F2 . f) (*) (T . f2) ) )
let F1, F2 be Functor of C1,C2; :: thesis: for T being Functor of C1,C2 st F1 is covariant & F2 is covariant holds
( T is_natural_transformation_of F1,F2 iff for f, f1, f2 being morphism of C1 st f1 is identity & f2 is identity & f1 |> f & f |> f2 holds
( T . f1 |> F1 . f & F2 . f |> T . f2 & T . f = (T . f1) (*) (F1 . f) & T . f = (F2 . f) (*) (T . f2) ) )
let T be Functor of C1,C2; :: thesis: ( F1 is covariant & F2 is covariant implies ( T is_natural_transformation_of F1,F2 iff for f, f1, f2 being morphism of C1 st f1 is identity & f2 is identity & f1 |> f & f |> f2 holds
( T . f1 |> F1 . f & F2 . f |> T . f2 & T . f = (T . f1) (*) (F1 . f) & T . f = (F2 . f) (*) (T . f2) ) ) )
assume A1: ( F1 is covariant & F2 is covariant ) ; :: thesis: ( T is_natural_transformation_of F1,F2 iff for f, f1, f2 being morphism of C1 st f1 is identity & f2 is identity & f1 |> f & f |> f2 holds
( T . f1 |> F1 . f & F2 . f |> T . f2 & T . f = (T . f1) (*) (F1 . f) & T . f = (F2 . f) (*) (T . f2) ) )

hereby :: thesis: ( ( for f, f1, f2 being morphism of C1 st f1 is identity & f2 is identity & f1 |> f & f |> f2 holds
( T . f1 |> F1 . f & F2 . f |> T . f2 & T . f = (T . f1) (*) (F1 . f) & T . f = (F2 . f) (*) (T . f2) ) ) implies T is_natural_transformation_of F1,F2 )

assume A2: T is_natural_transformation_of F1,F2 ; :: thesis: for f, f1, f2 being morphism of C1 st f1 is identity & f2 is identity & f1 |> f & f |> f2 holds
( T . f1 |> F1 . f & F2 . f |> T . f2 & T . f = (T . f1) (*) (F1 . f) & T . f = (F2 . f) (*) (T . f2) )
let f, f1, f2 be morphism of C1; :: thesis: ( f1 is identity & f2 is identity & f1 |> f & f |> f2 implies ( T . f1 |> F1 . f & F2 . f |> T . f2 & T . f = (T . f1) (*) (F1 . f) & T . f = (F2 . f) (*) (T . f2) ) )
assume A3: ( f1 is identity & f2 is identity ) ; :: thesis: ( f1 |> f & f |> f2 implies ( T . f1 |> F1 . f & F2 . f |> T . f2 & T . f = (T . f1) (*) (F1 . f) & T . f = (F2 . f) (*) (T . f2) ) )
assume A4: ( f1 |> f & f |> f2 ) ; :: thesis: ( T . f1 |> F1 . f & F2 . f |> T . f2 & T . f = (T . f1) (*) (F1 . f) & T . f = (F2 . f) (*) (T . f2) )
hence ( T . f1 |> F1 . f & F2 . f |> T . f2 ) by A2; :: thesis: ( T . f = (T . f1) (*) (F1 . f) & T . f = (F2 . f) (*) (T . f2) )
thus T . f = T . (f1 (*) f) by A3, A4, Th4
.= (T . f1) (*) (F1 . f) by A4, A2 ; :: thesis: T . f = (F2 . f) (*) (T . f2)
thus T . f = T . (f (*) f2) by A3, A4, Th4
.= (F2 . f) (*) (T . f2) by A4, A2 ; :: thesis: verum

end;

assume A5: for f, f1, f2 being morphism of C1 st f1 is identity & f2 is identity & f1 |> f & f |> f2 holds
( T . f1 |> F1 . f & F2 . f |> T . f2 & T . f = (T . f1) (*) (F1 . f) & T . f = (F2 . f) (*) (T . f2) ) ; :: thesis: T is_natural_transformation_of F1,F2
for g1, g2 being morphism of C1 st g1 |> g2 holds
( T . g1 |> F1 . g2 & F2 . g1 |> T . g2 & T . (g1 (*) g2) = (T . g1) (*) (F1 . g2) & T . (g1 (*) g2) = (F2 . g1) (*) (T . g2) )

proof

let g1, g2 be morphism of C1; :: thesis: ( g1 |> g2 implies ( T . g1 |> F1 . g2 & F2 . g1 |> T . g2 & T . (g1 (*) g2) = (T . g1) (*) (F1 . g2) & T . (g1 (*) g2) = (F2 . g1) (*) (T . g2) ) )
assume A6: g1 |> g2 ; :: thesis: ( T . g1 |> F1 . g2 & F2 . g1 |> T . g2 & T . (g1 (*) g2) = (T . g1) (*) (F1 . g2) & T . (g1 (*) g2) = (F2 . g1) (*) (T . g2) )
then A7: not C1 is empty by CAT_6:1;
then consider f1, f2 being morphism of C1 such that
A8: ( f1 is identity & f2 is identity ) and
A9: ( f1 |> g1 (*) g2 & g1 (*) g2 |> f2 ) by Th5;
consider g11 being morphism of C1 such that
A10: ( dom g1 = g11 & g1 |> g11 & g11 is identity ) by A7, CAT_6:def 18;
f1 |> g1 by A6, A9, Th3;
then A11: ( T . f1 |> F1 . g1 & T . g1 = (T . f1) (*) (F1 . g1) ) by A8, A10, A5;
A12: F1 . g1 |> F1 . g2 by A1, A6, Th13;
hence T . g1 |> F1 . g2 by A11, Th3; :: thesis: ( F2 . g1 |> T . g2 & T . (g1 (*) g2) = (T . g1) (*) (F1 . g2) & T . (g1 (*) g2) = (F2 . g1) (*) (T . g2) )
consider g22 being morphism of C1 such that
A13: ( cod g2 = g22 & g22 |> g2 & g22 is identity ) by A7, CAT_6:def 19;
g2 |> f2 by A6, A9, Th3;
then A14: ( F2 . g2 |> T . f2 & T . g2 = (F2 . g2) (*) (T . f2) ) by A13, A8, A5;
A15: F2 . g1 |> F2 . g2 by A1, A6, Th13;
hence F2 . g1 |> T . g2 by A14, Th3; :: thesis: ( T . (g1 (*) g2) = (T . g1) (*) (F1 . g2) & T . (g1 (*) g2) = (F2 . g1) (*) (T . g2) )
thus T . (g1 (*) g2) = (T . f1) (*) (F1 . (g1 (*) g2)) by A8, A9, A5
.= (T . f1) (*) ((F1 . g1) (*) (F1 . g2)) by A1, A6, Th13
.= (T . g1) (*) (F1 . g2) by A11, A12, Th1 ; :: thesis: T . (g1 (*) g2) = (F2 . g1) (*) (T . g2)
thus T . (g1 (*) g2) = (F2 . (g1 (*) g2)) (*) (T . f2) by A8, A9, A5
.= ((F2 . g1) (*) (F2 . g2)) (*) (T . f2) by A1, A6, Th13
.= (F2 . g1) (*) (T . g2) by A14, A15, Th1 ; :: thesis: verum

end;

hence T is_natural_transformation_of F1,F2 ; :: thesis: verum