let A, B, C be Category; :: thesis: for F1, F2 being Functor of A,B
for G1, G2 being Functor of B,C st F1 is_transformable_to F2 & G1 is_transformable_to G2 holds
G1 * F1 is_transformable_to G2 * F2
let F1, F2 be Functor of A,B; :: thesis: for G1, G2 being Functor of B,C st F1 is_transformable_to F2 & G1 is_transformable_to G2 holds
G1 * F1 is_transformable_to G2 * F2
let G1, G2 be Functor of B,C; :: thesis: ( F1 is_transformable_to F2 & G1 is_transformable_to G2 implies G1 * F1 is_transformable_to G2 * F2 )
assume that
A1: F1 is_transformable_to F2 and
A2: G1 is_transformable_to G2 ; :: thesis: G1 * F1 is_transformable_to G2 * F2
let a be Object of A; :: according to NATTRA_1:def 2 :: thesis: not Hom (((G1 * F1) . a),((G2 * F2) . a)) = {}
Hom ((F1 . a),(F2 . a)) <> {} by A1;
then A3: Hom ((G1 . (F1 . a)),(G1 . (F2 . a))) <> {} by CAT_1:84;
A4: ( G1 . (F1 . a) = (G1 * F1) . a & G2 . (F2 . a) = (G2 * F2) . a ) by CAT_1:76;
Hom ((G1 . (F2 . a)),(G2 . (F2 . a))) <> {} by A2;
hence not Hom (((G1 * F1) . a),((G2 * F2) . a)) = {} by A4, A3, CAT_1:24; :: thesis: verum