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