let A, B be Category; :: thesis: for f being Morphism of (Functors (A,B)) ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( F1 is_naturally_transformable_to F2 & dom f = F1 & cod f = F2 & f = [[F1,F2],t] )
let m be Morphism of (Functors (A,B)); :: thesis: ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( F1 is_naturally_transformable_to F2 & dom m = F1 & cod m = F2 & m = [[F1,F2],t] )
( Hom ((dom m),(cod m)) <> {} & m is Morphism of dom m, cod m ) by CAT_1:2, CAT_1:4;
then consider F, F1 being Functor of A,B, t being natural_transformation of F,F1 such that
A1: ( dom m = F & cod m = F1 ) and
A2: m = [[F,F1],t] by NATTRA_1:34;
take F ; :: thesis: ex F2 being Functor of A,B ex t being natural_transformation of F,F2 st
( F is_naturally_transformable_to F2 & dom m = F & cod m = F2 & m = [[F,F2],t] )
take F1 ; :: thesis: ex t being natural_transformation of F,F1 st
( F is_naturally_transformable_to F1 & dom m = F & cod m = F1 & m = [[F,F1],t] )
take t ; :: thesis: ( F is_naturally_transformable_to F1 & dom m = F & cod m = F1 & m = [[F,F1],t] )
the carrier' of (Functors (A,B)) = NatTrans (A,B) by NATTRA_1:def 17;
hence F is_naturally_transformable_to F1 by A2, NATTRA_1:32; :: thesis: ( dom m = F & cod m = F1 & m = [[F,F1],t] )
thus ( dom m = F & cod m = F1 & m = [[F,F1],t] ) by A1, A2; :: thesis: verum