let C1, C2 be category; 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 ; ( 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
; ( 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 ) }
; ( 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 = [[{},{}],{}]
; ( 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 ;
( x in X1 iff x = X2 )
hereby ( x = X2 implies x in X1 )
end;
assume A6:
x = X2
;
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;
verum
end;
hence
X1 = {X2}
by TARSKI:def 1; { [[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 ;
( 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 ( 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)] ) }
;
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;
verum
end;
assume A11:
x = [[X2,X2],X2]
;
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;
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; verum