set F = the Functor of A,B;
defpred S₁[ 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)):] & S₁[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 ; :: 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: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; :: thesis: verum