let A, B be Category; :: thesis: for F, F1 being Functor of A,B
for t being natural_transformation of F,F1
for f being Morphism of (Functors (A,B)) st f = [[F,F1],t] holds
( dom f = F & cod f = F1 )
let F, F1 be Functor of A,B; :: thesis: for t being natural_transformation of F,F1
for f being Morphism of (Functors (A,B)) st f = [[F,F1],t] holds
( dom f = F & cod f = F1 )
let t be natural_transformation of F,F1; :: thesis: for f being Morphism of (Functors (A,B)) st f = [[F,F1],t] holds
( dom f = F & cod f = F1 )
let f be Morphism of (Functors (A,B)); :: thesis: ( f = [[F,F1],t] implies ( dom f = F & cod f = F1 ) )
assume A1: f = [[F,F1],t] ; :: thesis: ( dom f = F & cod f = F1 )
thus dom f = (f `1) `1 by Def16
.= [F,F1] `1 by A1
.= F ; :: thesis: cod f = F1
thus cod f = (f `1) `2 by Def16
.= [F,F1] `2 by A1
.= F1 ; :: thesis: verum