let A, B, C be Category; :: thesis: for F being Functor of A,B
for G being Functor of A,C
for a being Object of A holds <:F,G:> . a = [(F . a),(G . a)]
let F be Functor of A,B; :: thesis: for G being Functor of A,C
for a being Object of A holds <:F,G:> . a = [(F . a),(G . a)]
let G be Functor of A,C; :: thesis: for a being Object of A holds <:F,G:> . a = [(F . a),(G . a)]
let a be Object of A; :: thesis: <:F,G:> . a = [(F . a),(G . a)]
<:F,G:> . (id a) = [(F . (id a)),(G . (id a))] by FUNCT_3:59
.= [(id (F . a)),(G . (id a))] by CAT_1:71
.= [(id (F . a)),(id (G . a))] by CAT_1:71
.= id [(F . a),(G . a)] by CAT_2:31 ;
hence <:F,G:> . a = [(F . a),(G . a)] by CAT_1:70; :: thesis: verum