let A, B be Category; 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; 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; ( 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]) <> {}
; 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; 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; ( [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 ) )
( 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]
;
( 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;
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; verum