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_transformable_to G1 & F2 is_transformable_to G2 holds
for t1 being transformation of F1,G1
for t2 being transformation of F2,G2
for a being Object of A holds <:t1,t2:> . a in Hom (<:F1,F2:> . a),(<:G1,G2:> . a)
let F1, G1 be Functor of A,B; :: thesis: for F2, G2 being Functor of A,C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds
for t1 being transformation of F1,G1
for t2 being transformation of F2,G2
for a being Object of A holds <:t1,t2:> . a in Hom (<:F1,F2:> . a),(<:G1,G2:> . a)
let F2, G2 be Functor of A,C; :: thesis: ( F1 is_transformable_to G1 & F2 is_transformable_to G2 implies for t1 being transformation of F1,G1
for t2 being transformation of F2,G2
for a being Object of A holds <:t1,t2:> . a in Hom (<:F1,F2:> . a),(<:G1,G2:> . a) )
assume A1: ( F1 is_transformable_to G1 & F2 is_transformable_to G2 ) ; :: thesis: for t1 being transformation of F1,G1
for t2 being transformation of F2,G2
for a being Object of A holds <:t1,t2:> . a in Hom (<:F1,F2:> . a),(<:G1,G2:> . a)
let t1 be transformation of F1,G1; :: thesis: for t2 being transformation of F2,G2
for a being Object of A holds <:t1,t2:> . a in Hom (<:F1,F2:> . a),(<:G1,G2:> . a)
let t2 be transformation of F2,G2; :: thesis: for a being Object of A holds <:t1,t2:> . a in Hom (<:F1,F2:> . a),(<:G1,G2:> . a)
let a be Object of A; :: thesis: <:t1,t2:> . a in Hom (<:F1,F2:> . a),(<:G1,G2:> . a)
A2: ( t1 . a in Hom (F1 . a),(G1 . a) & t2 . a in Hom (F2 . a),(G2 . a) ) by A1, ISOCAT_1:7;
( [(F1 . a),(F2 . a)] = <:F1,F2:> . a & [(G1 . a),(G2 . a)] = <:G1,G2:> . a & [(t1 . a),(t2 . a)] = <:t1,t2:> . a ) by A1, Lm2, Th43;
hence <:t1,t2:> . a in Hom (<:F1,F2:> . a),(<:G1,G2:> . a) by A2, Th16; :: thesis: verum