let A, B be Category; for a1, a2 being Object of A
for b1, b2 being Object of B
for f being Morphism of A
for g being Morphism of B st f in Hom (a1,a2) & g in Hom (b1,b2) holds
[f,g] in Hom ([a1,b1],[a2,b2])
let a1, a2 be Object of A; for b1, b2 being Object of B
for f being Morphism of A
for g being Morphism of B st f in Hom (a1,a2) & g in Hom (b1,b2) holds
[f,g] in Hom ([a1,b1],[a2,b2])
let b1, b2 be Object of B; for f being Morphism of A
for g being Morphism of B st f in Hom (a1,a2) & g in Hom (b1,b2) holds
[f,g] in Hom ([a1,b1],[a2,b2])
let f be Morphism of A; for g being Morphism of B st f in Hom (a1,a2) & g in Hom (b1,b2) holds
[f,g] in Hom ([a1,b1],[a2,b2])
let g be Morphism of B; ( f in Hom (a1,a2) & g in Hom (b1,b2) implies [f,g] in Hom ([a1,b1],[a2,b2]) )
assume
( f in Hom (a1,a2) & g in Hom (b1,b2) )
; [f,g] in Hom ([a1,b1],[a2,b2])
then
[f,g] in [:(Hom (a1,a2)),(Hom (b1,b2)):]
by ZFMISC_1:87;
hence
[f,g] in Hom ([a1,b1],[a2,b2])
by CAT_2:32; verum