consider F being Functor of A,B;
defpred S₁[ set ] 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 set holds
( x in T iff ( x in [:[:(Funct A,B),(Funct A,B):],(Funcs the carrier of A,the carrier' of B):] & S₁[x] ) ) from XBOOLE_0:sch 1();
F in Funct A,B by CAT_2:def 2;
then A2: [F,F] in [:(Funct A,B),(Funct A,B):] by ZFMISC_1:106;
id F in Funcs the carrier of A,the carrier' of B by FUNCT_2:11;
then [[F,F],(id F)] in [:[:(Funct A,B),(Funct A,B):],(Funcs the carrier of A,the carrier' of B):] by A2, ZFMISC_1:106;
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 Def15;
take T ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: ( 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 ; :: thesis: 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:11;
F1 in Funct A,B by CAT_2:def 2;
then [F1,F2] in [:(Funct A,B),(Funct A,B):] by A5, ZFMISC_1:106;
then x in [:[:(Funct A,B),(Funct A,B):],(Funcs the carrier of A,the carrier' of B):] by A3, A6, ZFMISC_1:106;
hence x in T by A1, A3, A4; :: thesis: verum