let B, A be Category; :: thesis: for F, F1, F2 being Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 holds
for t1 being transformation of F,F1 st ( for a, b being Object of A st Hom a,b <> {} holds
for f being Morphism of a,b holds (t1 . b) * (F . f) = (F1 . f) * (t1 . a) ) holds
for t2 being transformation of F1,F2 st ( for a, b being Object of A st Hom a,b <> {} holds
for f being Morphism of a,b holds (t2 . b) * (F1 . f) = (F2 . f) * (t2 . a) ) holds
for a, b being Object of A st Hom a,b <> {} holds
for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F . f) = (F2 . f) * ((t2 `*` t1) . a)
let F, F1, F2 be Functor of A,B; :: thesis: ( F is_transformable_to F1 & F1 is_transformable_to F2 implies for t1 being transformation of F,F1 st ( for a, b being Object of A st Hom a,b <> {} holds
for f being Morphism of a,b holds (t1 . b) * (F . f) = (F1 . f) * (t1 . a) ) holds
for t2 being transformation of F1,F2 st ( for a, b being Object of A st Hom a,b <> {} holds
for f being Morphism of a,b holds (t2 . b) * (F1 . f) = (F2 . f) * (t2 . a) ) holds
for a, b being Object of A st Hom a,b <> {} holds
for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F . f) = (F2 . f) * ((t2 `*` t1) . a) )
assume that
A1: F is_transformable_to F1 and
A2: F1 is_transformable_to F2 ; :: thesis: for t1 being transformation of F,F1 st ( for a, b being Object of A st Hom a,b <> {} holds
for f being Morphism of a,b holds (t1 . b) * (F . f) = (F1 . f) * (t1 . a) ) holds
for t2 being transformation of F1,F2 st ( for a, b being Object of A st Hom a,b <> {} holds
for f being Morphism of a,b holds (t2 . b) * (F1 . f) = (F2 . f) * (t2 . a) ) holds
for a, b being Object of A st Hom a,b <> {} holds
for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F . f) = (F2 . f) * ((t2 `*` t1) . a)
let t1 be transformation of F,F1; :: thesis: ( ( for a, b being Object of A st Hom a,b <> {} holds
for f being Morphism of a,b holds (t1 . b) * (F . f) = (F1 . f) * (t1 . a) ) implies for t2 being transformation of F1,F2 st ( for a, b being Object of A st Hom a,b <> {} holds
for f being Morphism of a,b holds (t2 . b) * (F1 . f) = (F2 . f) * (t2 . a) ) holds
for a, b being Object of A st Hom a,b <> {} holds
for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F . f) = (F2 . f) * ((t2 `*` t1) . a) )
assume A3: for a, b being Object of A st Hom a,b <> {} holds
for f being Morphism of a,b holds (t1 . b) * (F . f) = (F1 . f) * (t1 . a) ; :: thesis: for t2 being transformation of F1,F2 st ( for a, b being Object of A st Hom a,b <> {} holds
for f being Morphism of a,b holds (t2 . b) * (F1 . f) = (F2 . f) * (t2 . a) ) holds
for a, b being Object of A st Hom a,b <> {} holds
for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F . f) = (F2 . f) * ((t2 `*` t1) . a)
let t2 be transformation of F1,F2; :: thesis: ( ( for a, b being Object of A st Hom a,b <> {} holds
for f being Morphism of a,b holds (t2 . b) * (F1 . f) = (F2 . f) * (t2 . a) ) implies for a, b being Object of A st Hom a,b <> {} holds
for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F . f) = (F2 . f) * ((t2 `*` t1) . a) )
assume A4: for a, b being Object of A st Hom a,b <> {} holds
for f being Morphism of a,b holds (t2 . b) * (F1 . f) = (F2 . f) * (t2 . a) ; :: thesis: for a, b being Object of A st Hom a,b <> {} holds
for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F . f) = (F2 . f) * ((t2 `*` t1) . a)
let a, b be Object of A; :: thesis: ( Hom a,b <> {} implies for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F . f) = (F2 . f) * ((t2 `*` t1) . a) )
assume A5: Hom a,b <> {} ; :: thesis: for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F . f) = (F2 . f) * ((t2 `*` t1) . a)
then A6: ( Hom (F . a),(F . b) <> {} & Hom (F . b),(F1 . b) <> {} ) by A1, Def2, CAT_1:126;
A7: ( Hom (F . a),(F1 . a) <> {} & Hom (F1 . a),(F2 . a) <> {} ) by A1, A2, Def2;
A8: Hom (F1 . b),(F2 . b) <> {} by A2, Def2;
A9: Hom (F2 . a),(F2 . b) <> {} by A5, CAT_1:126;
A10: Hom (F1 . a),(F1 . b) <> {} by A5, CAT_1:126;
let f be Morphism of a,b; :: thesis: ((t2 `*` t1) . b) * (F . f) = (F2 . f) * ((t2 `*` t1) . a)
thus ((t2 `*` t1) . b) * (F . f) = ((t2 . b) * (t1 . b)) * (F . f) by A1, A2, Def6
.= (t2 . b) * ((t1 . b) * (F . f)) by A6, A8, CAT_1:54
.= (t2 . b) * ((F1 . f) * (t1 . a)) by A3, A5
.= ((t2 . b) * (F1 . f)) * (t1 . a) by A7, A8, A10, CAT_1:54
.= ((F2 . f) * (t2 . a)) * (t1 . a) by A4, A5
.= (F2 . f) * ((t2 . a) * (t1 . a)) by A7, A9, CAT_1:54
.= (F2 . f) * ((t2 `*` t1) . a) by A1, A2, Def6 ; :: thesis: verum