let A, B be Category; :: thesis: for a, b being Object of (Functors (A,B))
for f being Morphism of a,b st Hom (a,b) <> {} holds
ex F, F1 being Functor of A,B ex t being natural_transformation of F,F1 st
( a = F & b = F1 & f = [[F,F1],t] )
let a, b be Object of (Functors (A,B)); :: thesis: for f being Morphism of a,b st Hom (a,b) <> {} holds
ex F, F1 being Functor of A,B ex t being natural_transformation of F,F1 st
( a = F & b = F1 & f = [[F,F1],t] )
let f be Morphism of a,b; :: thesis: ( Hom (a,b) <> {} implies ex F, F1 being Functor of A,B ex t being natural_transformation of F,F1 st
( a = F & b = F1 & f = [[F,F1],t] ) )
assume A1: Hom (a,b) <> {} ; :: thesis: ex F, F1 being Functor of A,B ex t being natural_transformation of F,F1 st
( a = F & b = F1 & f = [[F,F1],t] )
the carrier' of (Functors (A,B)) = NatTrans (A,B) by Def16;
then consider F1, F2 being Functor of A,B, t being natural_transformation of F1,F2 such that
A2: f = [[F1,F2],t] and
F1 is_naturally_transformable_to F2 by Def14;
take F1 ; :: thesis: ex F1 being Functor of A,B ex t being natural_transformation of F1,F1 st
( a = F1 & b = F1 & f = [[F1,F1],t] )
take F2 ; :: thesis: ex t being natural_transformation of F1,F2 st
( a = F1 & b = F2 & f = [[F1,F2],t] )
take t ; :: thesis: ( a = F1 & b = F2 & f = [[F1,F2],t] )
thus a = dom f by A1, CAT_1:5
.= F1 by A2, Th29 ; :: thesis: ( b = F2 & f = [[F1,F2],t] )
thus b = cod f by A1, CAT_1:5
.= F2 by A2, Th29 ; :: thesis: f = [[F1,F2],t]
thus f = [[F1,F2],t] by A2; :: thesis: verum