set F = the Functor of A,B;
defpred S1[ object ] means ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( $1 = [[F1,F2],t] & F1 is_naturally_transformable_to F2 );
consider T being set such that
A1:
for x being object holds
( x in T iff ( x in [:[:(Funct (A,B)),(Funct (A,B)):],(Funcs ( the carrier of A, the carrier' of B)):] & S1[x] ) )
from XBOOLE_0:sch 1();
the Functor of A,B in Funct (A,B)
by CAT_2:def 2;
then A2:
[ the Functor of A,B, the Functor of A,B] in [:(Funct (A,B)),(Funct (A,B)):]
by ZFMISC_1:87;
id the Functor of A,B in Funcs ( the carrier of A, the carrier' of B)
by FUNCT_2:8;
then
[[ the Functor of A,B, the Functor of A,B],(id the Functor of A,B)] in [:[:(Funct (A,B)),(Funct (A,B)):],(Funcs ( the carrier of A, the carrier' of B)):]
by A2, ZFMISC_1:87;
then reconsider T = T as non empty set by A1;
for x being set st x in T holds
ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 )
by A1;
then reconsider T = T as NatTrans-DOMAIN of A,B by Def14;
take
T
; for x being set holds
( x in T iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) )
let x be set ; ( x in T iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) )
thus
( x in T implies ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) )
by A1; ( ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) implies x in T )
given F1, F2 being Functor of A,B, t being natural_transformation of F1,F2 such that A3:
x = [[F1,F2],t]
and
A4:
F1 is_naturally_transformable_to F2
; x in T
A5:
F2 in Funct (A,B)
by CAT_2:def 2;
A6:
t in Funcs ( the carrier of A, the carrier' of B)
by FUNCT_2:8;
F1 in Funct (A,B)
by CAT_2:def 2;
then
[F1,F2] in [:(Funct (A,B)),(Funct (A,B)):]
by A5, ZFMISC_1:87;
then
x in [:[:(Funct (A,B)),(Funct (A,B)):],(Funcs ( the carrier of A, the carrier' of B)):]
by A3, A6, ZFMISC_1:87;
hence
x in T
by A1, A3, A4; verum