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, Th41;
then consider F', F1', F2' being Functor of A,B, t' being natural_transformation of F',F1', t1' being natural_transformation of F1',F2' such that
A4: ( f = [[F',F1'],t'] & g = [[F1',F2'],t1'] ) and
A5: the Comp of (Functors A,B) . g,f = [[F',F2'],(t1' `*` t')] by Def18;
A6: ( [F',F1'] = [F,F1] & [F1',F2'] = [F1,F2] & t = t' & t1 = t1' ) by A1, A2, A4, ZFMISC_1:33;
then ( F = F' & F1 = F1' & F2 = F2' ) by ZFMISC_1:33;
hence g * f = [[F,F2],(t1 `*` t)] by A3, A5, A6, CAT_1:def 4; :: thesis: verum