let C, D, D' be Category; :: thesis: for T being Functor of C,D
for T' being Functor of C,D'
for c being Object of holds (Obj <:T,T':>) . c = [((Obj T) . c),((Obj T') . c)]
let T be Functor of C,D; :: thesis: for T' being Functor of C,D'
for c being Object of holds (Obj <:T,T':>) . c = [((Obj T) . c),((Obj T') . c)]
let T' be Functor of C,D'; :: thesis: for c being Object of holds (Obj <:T,T':>) . c = [((Obj T) . c),((Obj T') . c)]
let c be Object of ; :: thesis: (Obj <:T,T':>) . c = [((Obj T) . c),((Obj T') . c)]
A1: ( T . (id c) = id ((Obj T) . c) & T' . (id c) = id ((Obj T') . c) ) by CAT_1:104;
( <:T,T':> . (id c) = [(T . (id c)),(T' . (id c))] & [(id ((Obj T) . c)),(id ((Obj T') . c))] = id [((Obj T) . c),((Obj T') . c)] ) by Th41, FUNCT_3:79;
hence (Obj <:T,T':>) . c = [((Obj T) . c),((Obj T') . c)] by A1, CAT_1:103; :: thesis: verum