let A, B be Category; 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; 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; 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; 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)); ( 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]
; 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; verum