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 ) )
then A2: ( Hom a1,a2 <> {} & Hom b1,b2 <> {} ) by Th13;
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 ( [f,g] in Hom [a1,b1],[a2,b2] & Hom [a1,b1],[a2,b2] = [:(Hom a1,a2),(Hom b1,b2):] ) by A1, CAT_1:def 7, CAT_2:42;
then ( f in Hom a1,a2 & g in Hom b1,b2 ) by ZFMISC_1:106;
hence ( f is Morphism of a1,a2 & g is Morphism of b1,b2 ) by CAT_1:def 7; :: thesis: verum

end;

thus ( f is Morphism of a1,a2 & g is Morphism of b1,b2 implies [f,g] is Morphism of [a1,b1],[a2,b2] ) by A2, CAT_2:43; :: thesis: verum