let A, B be Category; :: thesis: ( A is discrete & B is discrete implies [:A,B:] is discrete )
assume that
A1: A is discrete and
A2: B is discrete ; :: thesis: [:A,B:] is discrete
let f be Morphism of [:A,B:]; :: according to NATTRA_1:def 19 :: thesis: ex a being Object of [:A,B:] st f = id a
consider f1 being Morphism of A, f2 being Morphism of B such that
A3: f = [f1,f2] by DOMAIN_1:9;
consider a being Object of A such that
A4: f1 = id a by A1, Def19;
consider b being Object of B such that
A5: f2 = id b by A2, Def19;
take [a,b] ; :: thesis: f = id [a,b]
thus f = id [a,b] by A3, A4, A5, CAT_2:41; :: thesis: verum