let A, B be Category; :: thesis: for a1, a2 being Object of A
for b1, b2 being Object of B st Hom ([a1,b1],[a2,b2]) <> {} holds
for f being Morphism of A
for g being Morphism of B holds
( [f,g] is Morphism of [a1,b1],[a2,b2] iff ( f is Morphism of a1,a2 & g is Morphism of b1,b2 ) )
let a1, a2 be Object of A; :: thesis: for b1, b2 being Object of B st Hom ([a1,b1],[a2,b2]) <> {} holds
for f being Morphism of A
for g being Morphism of B holds
( [f,g] is Morphism of [a1,b1],[a2,b2] iff ( f is Morphism of a1,a2 & g is Morphism of b1,b2 ) )
let b1, b2 be Object of B; :: thesis: ( Hom ([a1,b1],[a2,b2]) <> {} implies for f being Morphism of A
for g being Morphism of B holds
( [f,g] is Morphism of [a1,b1],[a2,b2] iff ( f is Morphism of a1,a2 & g is Morphism of b1,b2 ) ) )
assume A1: Hom ([a1,b1],[a2,b2]) <> {} ; :: thesis: for f being Morphism of A
for g being Morphism of B holds
( [f,g] is Morphism of [a1,b1],[a2,b2] iff ( f is Morphism of a1,a2 & g is Morphism of b1,b2 ) )
let f be Morphism of A; :: thesis: for g being Morphism of B holds
( [f,g] is Morphism of [a1,b1],[a2,b2] iff ( f is Morphism of a1,a2 & g is Morphism of b1,b2 ) )
let g be Morphism of B; :: thesis: ( [f,g] is Morphism of [a1,b1],[a2,b2] iff ( f is Morphism of a1,a2 & g is Morphism of b1,b2 ) )
thus ( [f,g] is Morphism of [a1,b1],[a2,b2] implies ( f is Morphism of a1,a2 & g is Morphism of b1,b2 ) ) :: thesis: ( f is Morphism of a1,a2 & g is Morphism of b1,b2 implies [f,g] is Morphism of [a1,b1],[a2,b2] )

proof

assume [f,g] is Morphism of [a1,b1],[a2,b2] ; :: thesis: ( f is Morphism of a1,a2 & g is Morphism of b1,b2 )
then A2: [f,g] in Hom ([a1,b1],[a2,b2]) by A1, CAT_1:def 5;
Hom ([a1,b1],[a2,b2]) = [:(Hom (a1,a2)),(Hom (b1,b2)):] by CAT_2:32;
then ( f in Hom (a1,a2) & g in Hom (b1,b2) ) by A2, ZFMISC_1:87;
hence ( f is Morphism of a1,a2 & g is Morphism of b1,b2 ) by CAT_1:def 5; :: thesis: verum

end;

( Hom (a1,a2) <> {} & Hom (b1,b2) <> {} ) by A1, Th9;
hence ( f is Morphism of a1,a2 & g is Morphism of b1,b2 implies [f,g] is Morphism of [a1,b1],[a2,b2] ) by CAT_2:33; :: thesis: verum