thus
[:A,B:] is quasi-discrete
NATTRA_1:def 20 [:A,B:] is pseudo-discrete proof
let a,
b be
Element of
[:A,B:];
NATTRA_1:def 18 ( Hom (a,b) <> {} implies a = b )
assume A1:
Hom (
a,
b)
<> {}
;
a = b
consider a1 being
Element of
A,
b1 being
Element of
B such that A2:
a = [a1,b1]
by DOMAIN_1:1;
consider a2 being
Element of
A,
b2 being
Element of
B such that A3:
b = [a2,b2]
by DOMAIN_1:1;
Hom (
a,
b)
= [:(Hom (a1,a2)),(Hom (b1,b2)):]
by A2, A3, CAT_2:32;
then
(
Hom (
a1,
a2)
<> {} &
Hom (
b1,
b2)
<> {} )
by A1;
then
(
a1 = a2 &
b1 = b2 )
by Def17;
hence
a = b
by A2, A3;
verum
end;
let a be Element of [:A,B:]; NATTRA_1:def 19 Hom (a,a) is trivial
consider a1 being Element of A, b1 being Element of B such that
A4:
a = [a1,b1]
by DOMAIN_1:1;
Hom (a,a) = [:(Hom (a1,a1)),(Hom (b1,b1)):]
by A4, CAT_2:32;
hence
Hom (a,a) is trivial
; verum