let A, B be Category; :: thesis: for a1, a2 being Object of A
for b1, b2 being Object of B holds
( ( Hom a1,a2 <> {} & Hom b1,b2 <> {} ) iff Hom [a1,b1],[a2,b2] <> {} )
let a1, a2 be Object of A; :: thesis: for b1, b2 being Object of B holds
( ( Hom a1,a2 <> {} & Hom b1,b2 <> {} ) iff Hom [a1,b1],[a2,b2] <> {} )
let b1, b2 be Object of B; :: thesis: ( ( Hom a1,a2 <> {} & Hom b1,b2 <> {} ) iff Hom [a1,b1],[a2,b2] <> {} )
Hom [a1,b1],[a2,b2] = [:(Hom a1,a2),(Hom b1,b2):] by CAT_2:42;
hence ( ( Hom a1,a2 <> {} & Hom b1,b2 <> {} ) iff Hom [a1,b1],[a2,b2] <> {} ) by ZFMISC_1:113; :: thesis: verum