let A, B be Category; 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; 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; ( ( 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:32;
hence
( ( Hom (a1,a2) <> {} & Hom (b1,b2) <> {} ) iff Hom ([a1,b1],[a2,b2]) <> {} )
by ZFMISC_1:90; verum