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