thus [:A,B:] is quasi-discrete :: according to NATTRA_1:def 20 :: thesis: [:A,B:] is pseudo-discrete

proof

let a, b be Element of [:A,B:]; :: according to NATTRA_1:def 18 :: thesis: ( Hom (a,b) <> {} implies a = b )
assume A1: Hom (a,b) <> {} ; :: thesis: 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; :: thesis: verum

end;

let a be Element of [:A,B:]; :: according to NATTRA_1:def 19 :: thesis: 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 ; :: thesis: verum