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