consider T being natural_transformation of F1,F2 such that
A3: ( T is_natural_transformation_of F1,F2 & ( for f, f1, f2 being morphism of C st f1 is identity & f2 is identity & f |> f1 & f2 |> f holds
T . f = ((T2 . f2) (*) (F . f)) (*) (T1 . f1) ) ) by A1, A2, Lm3;
take T ; :: thesis: for f, f1, f2 being morphism of C st f1 is identity & f2 is identity & f |> f1 & f2 |> f holds
T . f = ((T2 . f2) (*) (F . f)) (*) (T1 . f1)
thus for f, f1, f2 being morphism of C st f1 is identity & f2 is identity & f |> f1 & f2 |> f holds
T . f = ((T2 . f2) (*) (F . f)) (*) (T1 . f1) by A3; :: thesis: verum