let A, B, C be non empty transitive with_units AltCatStr ; :: thesis: for F1, F2 being covariant Functor of A,B
for G1, G2 being covariant 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 covariant Functor of A,B; :: thesis: for G1, G2 being covariant 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 covariant Functor of B,C; :: thesis: ( F1 is_transformable_to F2 & G1 is_transformable_to G2 implies G1 * F1 is_transformable_to G2 * F2 )
assume A1: for a being object of A holds <^(F1 . a),(F2 . a)^> <> {} ; :: according to FUNCTOR2:def 1 :: thesis: ( not G1 is_transformable_to G2 or G1 * F1 is_transformable_to G2 * F2 )
assume A2: for a being object of B holds <^(G1 . a),(G2 . a)^> <> {} ; :: according to FUNCTOR2:def 1 :: thesis: G1 * F1 is_transformable_to G2 * F2
let a be object of A; :: according to FUNCTOR2:def 1 :: thesis: not <^((G1 * F1) . a),((G2 * F2) . a)^> = {}
A3: ( (G1 * F1) . a = G1 . (F1 . a) & (G2 * F2) . a = G2 . (F2 . a) ) by FUNCTOR0:34;
A4: <^(G1 . (F2 . a)),(G2 . (F2 . a))^> <> {} by A2;
<^(F1 . a),(F2 . a)^> <> {} by A1;
then <^(G1 . (F1 . a)),(G1 . (F2 . a))^> <> {} by FUNCTOR0:def 19;
hence not <^((G1 * F1) . a),((G2 * F2) . a)^> = {} by A3, A4, ALTCAT_1:def 4; :: thesis: verum