let A, B be Category; 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; 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; ( 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; ( [[F1,F2],t1] in NatTrans (A,B) implies F1 is_naturally_transformable_to F2 )
assume
[[F1,F2],t1] in NatTrans (A,B)
; 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; verum