let C1, C2 be category; :: thesis: for X1, X2 being set st C1 is empty & X1 = { [[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 ) } & X2 = [[{},{}],{}] holds
( X1 = {X2} & { [[x2,x1],x3] where x1, x2, x3 is Element of X1 : 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)] ) } = {[[X2,X2],X2]} )
let X1, X2 be set ; :: thesis: ( C1 is empty & X1 = { [[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 ) } & X2 = [[{},{}],{}] implies ( X1 = {X2} & { [[x2,x1],x3] where x1, x2, x3 is Element of X1 : 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)] ) } = {[[X2,X2],X2]} ) )
assume A1: C1 is empty ; :: thesis: ( not X1 = { [[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 not X2 = [[{},{}],{}] or ( X1 = {X2} & { [[x2,x1],x3] where x1, x2, x3 is Element of X1 : 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)] ) } = {[[X2,X2],X2]} ) )
assume A2: X1 = { [[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: ( not X2 = [[{},{}],{}] or ( X1 = {X2} & { [[x2,x1],x3] where x1, x2, x3 is Element of X1 : 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)] ) } = {[[X2,X2],X2]} ) )
assume A3: X2 = [[{},{}],{}] ; :: thesis: ( X1 = {X2} & { [[x2,x1],x3] where x1, x2, x3 is Element of X1 : 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)] ) } = {[[X2,X2],X2]} )
set Y = { [[x2,x1],x3] where x1, x2, x3 is Element of X1 : 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)] ) } ;
A4: for x being object holds
( x in X1 iff x = X2 )

proof

let x be object ; :: thesis: ( x in X1 iff x = X2 )

hereby :: thesis: ( x = X2 implies x in X1 )

assume x in X1 ; :: thesis: x = X2
then 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 A2;
( F1 = {} & F2 = {} & T = {} ) by A1;
hence x = X2 by A3, A5; :: thesis: verum

end;

assume A6: x = X2 ; :: thesis: x in X1
reconsider CA = C1 as empty category by A1;
set F = the covariant Functor of CA,C2;
reconsider F = the covariant Functor of CA,C2 as Functor of C1,C2 ;
A7: F is_natural_transformation_of F,F by Th61;
A8: F is_naturally_transformable_to F by Th61;
then reconsider T = F as natural_transformation of F,F by A7, Def26;
[[F,F],T] in X1 by A8, A2;
hence x in X1 by A3, A6; :: thesis: verum

end;

hence X1 = {X2} by TARSKI:def 1; :: thesis: { [[x2,x1],x3] where x1, x2, x3 is Element of X1 : 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)] ) } = {[[X2,X2],X2]}
for x being object holds
( x in { [[x2,x1],x3] where x1, x2, x3 is Element of X1 : 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)] ) } iff x = [[X2,X2],X2] )

proof

let x be object ; :: thesis: ( x in { [[x2,x1],x3] where x1, x2, x3 is Element of X1 : 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)] ) } iff x = [[X2,X2],X2] )

hereby :: thesis: ( x = [[X2,X2],X2] implies x in { [[x2,x1],x3] where x1, x2, x3 is Element of X1 : 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 x in { [[x2,x1],x3] where x1, x2, x3 is Element of X1 : 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: x = [[X2,X2],X2]
then consider x1, x2, x3 being Element of X1 such that
A9: ( 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)] ) ) ;
consider F1, F2, F3 being Functor of C1,C2, T1 being natural_transformation of F1,F2, T2 being natural_transformation of F2,F3 such that
A10: ( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) by A9;
( F1 = {} & F2 = {} & F3 = {} & T1 = {} & T2 = {} & T2 `*` T1 = {} ) by A1;
hence x = [[X2,X2],X2] by A9, A3, A10; :: thesis: verum

end;

assume A11: x = [[X2,X2],X2] ; :: thesis: x in { [[x2,x1],x3] where x1, x2, x3 is Element of X1 : 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)] ) }
reconsider CA = C1 as empty category by A1;
set F = the covariant Functor of CA,C2;
reconsider F = the covariant Functor of CA,C2 as Functor of C1,C2 ;
A12: F is_natural_transformation_of F,F by Th61;
F is_naturally_transformable_to F by Th61;
then reconsider T = F as natural_transformation of F,F by A12, Def26;
reconsider F1 = F, F2 = F, F3 = F as Functor of C1,C2 ;
reconsider T1 = T as natural_transformation of F1,F2 ;
reconsider T2 = T as natural_transformation of F2,F3 ;
A13: T2 `*` T1 = {} ;
reconsider x1 = [[F1,F2],T1] as Element of X1 by A3, A4;
reconsider x2 = [[F2,F3],T2] as Element of X1 by A3, A4;
reconsider x3 = [[F1,F3],(T2 `*` T1)] as Element of X1 by A3, A13, A4;
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)] ) ;
hence x in { [[x2,x1],x3] where x1, x2, x3 is Element of X1 : 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 A11, A13, A3; :: thesis: verum

end;

hence { [[x2,x1],x3] where x1, x2, x3 is Element of X1 : 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)] ) } = {[[X2,X2],X2]} by TARSKI:def 1; :: thesis: verum