let A, B, C be Category; 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; 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; for a being Object of A holds <:F,G:> . a = [(F . a),(G . a)]
let a be Object of A; <: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; verum