let A, B be Category; :: thesis: for F, F1, F2 being Functor of A,B
for t being natural_transformation of F,F1
for t1 being natural_transformation of F1,F2
for f, g being Morphism of (Functors (A,B)) st f = [[F,F1],t] & g = [[F1,F2],t1] holds
g (*) f = [[F,F2],(t1 `*` t)]
let F, F1, F2 be Functor of A,B; :: thesis: for t being natural_transformation of F,F1
for t1 being natural_transformation of F1,F2
for f, g being Morphism of (Functors (A,B)) st f = [[F,F1],t] & g = [[F1,F2],t1] holds
g (*) f = [[F,F2],(t1 `*` t)]
let t be natural_transformation of F,F1; :: thesis: for t1 being natural_transformation of F1,F2
for f, g being Morphism of (Functors (A,B)) st f = [[F,F1],t] & g = [[F1,F2],t1] holds
g (*) f = [[F,F2],(t1 `*` t)]
let t1 be natural_transformation of F1,F2; :: thesis: for f, g being Morphism of (Functors (A,B)) st f = [[F,F1],t] & g = [[F1,F2],t1] holds
g (*) f = [[F,F2],(t1 `*` t)]
let f, g be Morphism of (Functors (A,B)); :: thesis: ( f = [[F,F1],t] & g = [[F1,F2],t1] implies g (*) f = [[F,F2],(t1 `*` t)] )
assume that
A1: f = [[F,F1],t] and
A2: g = [[F1,F2],t1] ; :: thesis: g (*) f = [[F,F2],(t1 `*` t)]
A3: [g,f] in dom the Comp of (Functors (A,B)) by A1, A2, Th31;
then consider F9, F19, F29 being Functor of A,B, t9 being natural_transformation of F9,F19, t19 being natural_transformation of F19,F29 such that
A4: f = [[F9,F19],t9] and
A5: g = [[F19,F29],t19] and
A6: the Comp of (Functors (A,B)) . (g,f) = [[F9,F29],(t19 `*` t9)] by Def16;
A7: t1 = t19 by A2, A5, XTUPLE_0:1;
A8: [F9,F19] = [F,F1] by A1, A4, XTUPLE_0:1;
then A9: F = F9 by XTUPLE_0:1;
[F19,F29] = [F1,F2] by A2, A5, XTUPLE_0:1;
then A10: F2 = F29 by XTUPLE_0:1;
A11: F1 = F19 by A8, XTUPLE_0:1;
t = t9 by A1, A4, XTUPLE_0:1;
hence g (*) f = [[F,F2],(t1 `*` t)] by A3, A6, A7, A9, A11, A10, CAT_1:def 1; :: thesis: verum