let IT1, IT2 be 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
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)
; ( 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)
; IT1 = IT2
for x being object st x in the carrier of C holds
IT1 . x = IT2 . x
proof
let x be
object ;
( x in the carrier of C implies IT1 . x = IT2 . x )
assume A6:
x in the
carrier of
C
;
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
;
verum
end;
hence
IT1 = IT2
by FUNCT_2:12; verum