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:87;
hence [f,g] in Hom ([a1,b1],[a2,b2]) by CAT_2:32; :: thesis: verum