let A, B be Category; :: thesis: for F2, F3, F, F1 being Functor of A,B
for t being natural_transformation of F,F1
for t' being natural_transformation of F2,F3
for f, g being Morphism of (Functors A,B) st f = [[F,F1],t] & g = [[F2,F3],t'] holds
( [g,f] in dom the Comp of (Functors A,B) iff F1 = F2 )
let F2, F3, F, F1 be Functor of A,B; :: thesis: for t being natural_transformation of F,F1
for t' being natural_transformation of F2,F3
for f, g being Morphism of (Functors A,B) st f = [[F,F1],t] & g = [[F2,F3],t'] holds
( [g,f] in dom the Comp of (Functors A,B) iff F1 = F2 )
let t be natural_transformation of F,F1; :: thesis: for t' being natural_transformation of F2,F3
for f, g being Morphism of (Functors A,B) st f = [[F,F1],t] & g = [[F2,F3],t'] holds
( [g,f] in dom the Comp of (Functors A,B) iff F1 = F2 )
let t' be natural_transformation of F2,F3; :: thesis: for f, g being Morphism of (Functors A,B) st f = [[F,F1],t] & g = [[F2,F3],t'] 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],t'] 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],t'] ; :: 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 F', F1', F2' being Functor of A,B, t' being natural_transformation of F',F1', t1' being natural_transformation of F1',F2' such that
A3: ( f = [[F',F1'],t'] & g = [[F1',F2'],t1'] ) and
the Comp of (Functors A,B) . [g,f] = [[F',F2'],(t1' `*` t')] by Def18;
thus F1 = [F,F1] `2 by MCART_1:7
.= ([[F,F1],t] `1 ) `2 by MCART_1:7
.= [F',F1'] `2 by A1, A3, MCART_1:7
.= F1' by MCART_1:7
.= [F1',F2'] `1 by MCART_1:7
.= ([[F1',F2'],t1'] `1 ) `1 by MCART_1:7
.= [F2,F3] `1 by A2, A3, MCART_1:7
.= F2 by MCART_1:7 ; :: thesis: verum

end;

( dom g = F2 & cod f = F1 ) by A1, A2, Th39;
hence ( F1 = F2 implies [g,f] in dom the Comp of (Functors A,B) ) by Def18; :: thesis: verum