let A, B, C be Category; :: thesis: for F1, F2, G1, G2 being Functor of A,[:B,C:] st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds
for s being natural_transformation of F1,F2
for t being natural_transformation of G1,G2 st Pr1 s = Pr1 t & Pr2 s = Pr2 t holds
s = t
let F1, F2, G1, G2 be Functor of A,[:B,C:]; :: thesis: ( F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 implies for s being natural_transformation of F1,F2
for t being natural_transformation of G1,G2 st Pr1 s = Pr1 t & Pr2 s = Pr2 t holds
s = t )
assume that
A1: F1 is_naturally_transformable_to F2 and
A2: G1 is_naturally_transformable_to G2 ; :: thesis: for s being natural_transformation of F1,F2
for t being natural_transformation of G1,G2 st Pr1 s = Pr1 t & Pr2 s = Pr2 t holds
s = t
let s be natural_transformation of F1,F2; :: thesis: for t being natural_transformation of G1,G2 st Pr1 s = Pr1 t & Pr2 s = Pr2 t holds
s = t
let t be natural_transformation of G1,G2; :: thesis: ( Pr1 s = Pr1 t & Pr2 s = Pr2 t implies s = t )
assume that
A3: Pr1 s = Pr1 t and
A4: Pr2 s = Pr2 t ; :: thesis: s = t
reconsider S = s, T = t as Function of the carrier of A,[: the carrier' of B, the carrier' of C:] ;
A5: (pr2 ( the carrier' of B, the carrier' of C)) * S = (pr2 (B,C)) * S
.= Pr2 s by A1, Th28
.= (pr2 (B,C)) * T by A2, A4, Th28
.= (pr2 ( the carrier' of B, the carrier' of C)) * T ;
(pr1 ( the carrier' of B, the carrier' of C)) * S = (pr1 (B,C)) * S
.= Pr1 s by A1, Th28
.= (pr1 (B,C)) * T by A2, A3, Th28
.= (pr1 ( the carrier' of B, the carrier' of C)) * T ;
hence s = t by A5, FUNCT_3:80; :: thesis: verum