let C, D, D9 be Category; :: thesis: for T being Functor of C,D
for T9 being Functor of C,D9
for c being Object of C holds (Obj <:T,T9:>) . c = [((Obj T) . c),((Obj T9) . c)]
let T be Functor of C,D; :: thesis: for T9 being Functor of C,D9
for c being Object of C holds (Obj <:T,T9:>) . c = [((Obj T) . c),((Obj T9) . c)]
let T9 be Functor of C,D9; :: thesis: for c being Object of C holds (Obj <:T,T9:>) . c = [((Obj T) . c),((Obj T9) . c)]
let c be Object of C; :: thesis: (Obj <:T,T9:>) . c = [((Obj T) . c),((Obj T9) . c)]
A1: ( T . (id c) = id ((Obj T) . c) & T9 . (id c) = id ((Obj T9) . c) ) by CAT_1:68;
( <:T,T9:> . (id c) = [(T . (id c)),(T9 . (id c))] & [(id ((Obj T) . c)),(id ((Obj T9) . c))] = id [((Obj T) . c),((Obj T9) . c)] ) by Th25, FUNCT_3:59;
hence (Obj <:T,T9:>) . c = [((Obj T) . c),((Obj T9) . c)] by A1, CAT_1:67; :: thesis: verum