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