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

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

proof

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

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