let A, B be Category; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: [f,g] in Hom [a1,b1],[a2,b2]
then [f,g] in [:(Hom a1,a2),(Hom b1,b2):] by ZFMISC_1:106;
hence [f,g] in Hom [a1,b1],[a2,b2] by CAT_2:42; :: thesis: verum