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