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 Def18
.= [F,F1] `1 by A1, MCART_1:7
.= F by MCART_1:7 ; :: thesis: cod f = F1
thus cod f = (f `1 ) `2 by Def18
.= [F,F1] `2 by A1, MCART_1:7
.= F1 by MCART_1:7 ; :: thesis: verum