let A, B be Category; for F, F1, F2, F3 being Functor of A,B
for t being natural_transformation of F,F1
for t9 being natural_transformation of F2,F3
for f, g being Morphism of (Functors (A,B)) st f = [[F,F1],t] & g = [[F2,F3],t9] holds
( [g,f] in dom the Comp of (Functors (A,B)) iff F1 = F2 )
let F, F1, F2, F3 be Functor of A,B; for t being natural_transformation of F,F1
for t9 being natural_transformation of F2,F3
for f, g being Morphism of (Functors (A,B)) st f = [[F,F1],t] & g = [[F2,F3],t9] holds
( [g,f] in dom the Comp of (Functors (A,B)) iff F1 = F2 )
let t be natural_transformation of F,F1; for t9 being natural_transformation of F2,F3
for f, g being Morphism of (Functors (A,B)) st f = [[F,F1],t] & g = [[F2,F3],t9] holds
( [g,f] in dom the Comp of (Functors (A,B)) iff F1 = F2 )
let t9 be natural_transformation of F2,F3; for f, g being Morphism of (Functors (A,B)) st f = [[F,F1],t] & g = [[F2,F3],t9] holds
( [g,f] in dom the Comp of (Functors (A,B)) iff F1 = F2 )
let f, g be Morphism of (Functors (A,B)); ( f = [[F,F1],t] & g = [[F2,F3],t9] implies ( [g,f] in dom the Comp of (Functors (A,B)) iff F1 = F2 ) )
assume that
A1:
f = [[F,F1],t]
and
A2:
g = [[F2,F3],t9]
; ( [g,f] in dom the Comp of (Functors (A,B)) iff F1 = F2 )
thus
( [g,f] in dom the Comp of (Functors (A,B)) implies F1 = F2 )
( F1 = F2 implies [g,f] in dom the Comp of (Functors (A,B)) )proof
assume
[g,f] in dom the
Comp of
(Functors (A,B))
;
F1 = F2
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 A3:
f = [[F9,F19],t9]
and A4:
g = [[F19,F29],t19]
and
the
Comp of
(Functors (A,B)) . [g,f] = [[F9,F29],(t19 `*` t9)]
by Def16;
thus F1 =
([[F,F1],t] `1) `2
.=
([[F9,F19],t9] `1) `2
by A1, A3
.=
[F9,F19] `2
.=
([[F19,F29],t19] `1) `1
.=
[F2,F3] `1
by A2, A4
.=
F2
;
verum
end;
A5:
cod f = F1
by A1, Th29;
dom g = F2
by A2, Th29;
hence
( F1 = F2 implies [g,f] in dom the Comp of (Functors (A,B)) )
by A5, Def16; verum