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 Def18;
then consider F1, F2 being Functor of A,B, t being natural_transformation of F1,F2 such that
A2: ( f = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) by Def15;
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:23
.= F1 by A2, Th39 ; :: thesis: ( b = F2 & f = [[F1,F2],t] )
thus b = cod f by A1, CAT_1:23
.= F2 by A2, Th39 ; :: thesis: f = [[F1,F2],t]
thus f = [[F1,F2],t] by A2; :: thesis: verum