let IT1, IT2 be natural_transformation of F1,F2; :: thesis: ( ( for f, f1, f2 being morphism of C st f1 is identity & f2 is identity & f |> f1 & f2 |> f holds
IT1 . f = ((T2 . f2) (*) (F . f)) (*) (T1 . f1) ) & ( for f, f1, f2 being morphism of C st f1 is identity & f2 is identity & f |> f1 & f2 |> f holds
IT2 . f = ((T2 . f2) (*) (F . f)) (*) (T1 . f1) ) implies IT1 = IT2 )
assume A4: for f, f1, f2 being morphism of C st f1 is identity & f2 is identity & f |> f1 & f2 |> f holds
IT1 . f = ((T2 . f2) (*) (F . f)) (*) (T1 . f1) ; :: thesis: ( ex f, f1, f2 being morphism of C st
( f1 is identity & f2 is identity & f |> f1 & f2 |> f & not IT2 . f = ((T2 . f2) (*) (F . f)) (*) (T1 . f1) ) or IT1 = IT2 )
assume A5: for f, f1, f2 being morphism of C st f1 is identity & f2 is identity & f |> f1 & f2 |> f holds
IT2 . f = ((T2 . f2) (*) (F . f)) (*) (T1 . f1) ; :: thesis: IT1 = IT2
for x being object st x in the carrier of C holds
IT1 . x = IT2 . x

proof

let x be object ; :: thesis: ( x in the carrier of C implies IT1 . x = IT2 . x )
assume A6: x in the carrier of C ; :: thesis: IT1 . x = IT2 . x
reconsider f = x as morphism of C by A6, CAT_6:def 1;
consider f2 being morphism of C such that
A7: ( f2 |> f & f2 is left_identity ) by A6, CAT_6:def 6, CAT_6:def 12;
consider f1 being morphism of C such that
A8: ( f |> f1 & f1 is right_identity ) by A6, CAT_6:def 7, CAT_6:def 12;
( f1 is left_identity & f2 is right_identity ) by A7, A8, CAT_6:9;
then A9: ( f1 is identity & f2 is identity ) by A7, A8, CAT_6:def 14;
A10: not C is empty by A6;
hence IT1 . x = IT1 . f by CAT_6:def 21
.= ((T2 . f2) (*) (F . f)) (*) (T1 . f1) by A4, A7, A8, A9
.= IT2 . f by A5, A7, A8, A9
.= IT2 . x by A10, CAT_6:def 21 ;
:: thesis: verum

end;

hence IT1 = IT2 by FUNCT_2:12; :: thesis: verum