let C1, C2 be category; 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 ; ( 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 )
; ( 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 ) }
; ( 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 = {}
{ [[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
{ [[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)] ) } = {}
verumproof
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)] ) } <> {}
;
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;
verum
end;