let A, B be Category; :: thesis: for F1, F2 being Functor of A,B
for t1 being natural_transformation of F1,F2 holds
( F1 is_naturally_transformable_to F2 iff [[F1,F2],t1] in NatTrans A,B )
let F1, F2 be Functor of A,B; :: thesis: for t1 being natural_transformation of F1,F2 holds
( F1 is_naturally_transformable_to F2 iff [[F1,F2],t1] in NatTrans A,B )
let t1 be natural_transformation of F1,F2; :: thesis: ( F1 is_naturally_transformable_to F2 iff [[F1,F2],t1] in NatTrans A,B )
thus ( F1 is_naturally_transformable_to F2 implies [[F1,F2],t1] in NatTrans A,B ) by Def16; :: thesis: ( [[F1,F2],t1] in NatTrans A,B implies F1 is_naturally_transformable_to F2 )
assume [[F1,F2],t1] in NatTrans A,B ; :: thesis: F1 is_naturally_transformable_to F2
then consider F19, F29 being Functor of A,B, t being natural_transformation of F19,F29 such that
A1: [[F1,F2],t1] = [[F19,F29],t] and
A2: F19 is_naturally_transformable_to F29 by Def16;
A3: [F1,F2] = [F19,F29] by A1, ZFMISC_1:33;
then F1 = F19 by ZFMISC_1:33;
hence F1 is_naturally_transformable_to F2 by A2, A3, ZFMISC_1:33; :: thesis: verum