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