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 Def15; :: 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 Def15;
A3: [F1,F2] = [F19,F29] by A1, XTUPLE_0:1;
then F1 = F19 by XTUPLE_0:1;
hence F1 is_naturally_transformable_to F2 by A2, A3, XTUPLE_0:1; :: thesis: verum