let A, B, C be Category; :: thesis: for F1, G1 being Functor of A,B
for F2, G2 being Functor of A,C st F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 holds
for t1 being natural_transformation of F1,G1
for t2 being natural_transformation of F2,G2 holds
( Pr1 <:t1,t2:> = t1 & Pr2 <:t1,t2:> = t2 )
let F1, G1 be Functor of A,B; :: thesis: for F2, G2 being Functor of A,C st F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 holds
for t1 being natural_transformation of F1,G1
for t2 being natural_transformation of F2,G2 holds
( Pr1 <:t1,t2:> = t1 & Pr2 <:t1,t2:> = t2 )
let F2, G2 be Functor of A,C; :: thesis: ( F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 implies for t1 being natural_transformation of F1,G1
for t2 being natural_transformation of F2,G2 holds
( Pr1 <:t1,t2:> = t1 & Pr2 <:t1,t2:> = t2 ) )
assume A1: ( F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 ) ; :: thesis: for t1 being natural_transformation of F1,G1
for t2 being natural_transformation of F2,G2 holds
( Pr1 <:t1,t2:> = t1 & Pr2 <:t1,t2:> = t2 )
A2: ( F1 is_transformable_to G1 & F2 is_transformable_to G2 ) by A1;
let t1 be natural_transformation of F1,G1; :: thesis: for t2 being natural_transformation of F2,G2 holds
( Pr1 <:t1,t2:> = t1 & Pr2 <:t1,t2:> = t2 )
let t2 be natural_transformation of F2,G2; :: thesis: ( Pr1 <:t1,t2:> = t1 & Pr2 <:t1,t2:> = t2 )
reconsider s = t1 as Function of the carrier of A, the carrier' of B ;
<:F1,F2:> is_naturally_transformable_to <:G1,G2:> by A1, Th36;
then A3: <:F1,F2:> is_transformable_to <:G1,G2:> ;
thus Pr1 <:t1,t2:> = (pr1 (B,C)) * <:t1,t2:> by A1, Th36, ISOCAT_1:def 7
.= (pr1 (B,C)) * <:t1,t2:> by A3, ISOCAT_1:def 5
.= (pr1 (B,C)) * <:t1,t2:> by A1, Def12
.= (pr1 (B,C)) * <:s,t2:> by A2, Def11
.= (pr1 ( the carrier' of B, the carrier' of C)) * <:s,t2:>
.= t1 by FUNCT_3:62 ; :: thesis: Pr2 <:t1,t2:> = t2
thus Pr2 <:t1,t2:> = (pr2 (B,C)) * <:t1,t2:> by A1, Th36, ISOCAT_1:def 7
.= (pr2 (B,C)) * <:t1,t2:> by A3, ISOCAT_1:def 5
.= (pr2 (B,C)) * <:t1,t2:> by A1, Def12
.= (pr2 (B,C)) * <:s,t2:> by A2, Def11
.= (pr2 ( the carrier' of B, the carrier' of C)) * <:s,t2:>
.= t2 by FUNCT_3:62 ; :: thesis: verum