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 F1', F2' being Functor of A,B, t being natural_transformation of F1',F2' such that
A1: ( [[F1,F2],t1] = [[F1',F2'],t] & F1' is_naturally_transformable_to F2' ) by Def16;
[F1,F2] = [F1',F2'] by A1, ZFMISC_1:33;
then ( F1 = F1' & F2 = F2' ) by ZFMISC_1:33;
hence F1 is_naturally_transformable_to F2 by A1; :: thesis: verum