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:4;
A3: ( [(F1 . a),(F2 . a)] = <:F1,F2:> . a & [(G1 . a),(G2 . a)] = <:G1,G2:> . a ) by Th33;
[(t1 . a),(t2 . a)] = <:t1,t2:> . a by A1, Lm2;
hence <:t1,t2:> . a in Hom ((<:F1,F2:> . a),(<:G1,G2:> . a)) by A2, A3, Th12; :: thesis: verum