let C1, C2 be category; :: thesis: for X being set st not C1 is empty & C2 is empty & X = { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } holds
( X = {} & { [[x2,x1],x3] where x1, x2, x3 is Element of X : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } = {} )
let X be set ; :: thesis: ( not C1 is empty & C2 is empty & X = { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } implies ( X = {} & { [[x2,x1],x3] where x1, x2, x3 is Element of X : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } = {} ) )
assume A1: ( not C1 is empty & C2 is empty ) ; :: thesis: ( not X = { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } or ( X = {} & { [[x2,x1],x3] where x1, x2, x3 is Element of X : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } = {} ) )
assume A2: X = { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } ; :: thesis: ( X = {} & { [[x2,x1],x3] where x1, x2, x3 is Element of X : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } = {} )
set Y = { [[x2,x1],x3] where x1, x2, x3 is Element of X : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } ;
thus A3: X = {} :: thesis: { [[x2,x1],x3] where x1, x2, x3 is Element of X : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } = {}

proof

assume X <> {} ; :: thesis: contradiction
then consider x being object such that
A4: x in X by XBOOLE_0:def 1;
consider F1, F2 being Functor of C1,C2, T being natural_transformation of F1,F2 such that
A5: ( x = [[F1,F2],T] & F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) by A4, A2;
thus contradiction by A5, A1, CAT_6:31; :: thesis: verum

end;

thus { [[x2,x1],x3] where x1, x2, x3 is Element of X : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } = {} :: thesis: verum

proof

assume { [[x2,x1],x3] where x1, x2, x3 is Element of X : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } <> {} ; :: thesis: contradiction
then consider x being object such that
A6: x in { [[x2,x1],x3] where x1, x2, x3 is Element of X : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } by XBOOLE_0:def 1;
consider x1, x2, x3 being Element of X such that
A7: ( x = [[x2,x1],x3] & ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) ) by A6;
thus contradiction by A7, A3; :: thesis: verum

end;