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 ; :: according to NATTRA_1:def 19 :: thesis: ex a being Object of st f = id a
consider f1 being Morphism of , f2 being Morphism of such that
A3: f = [f1,f2] by DOMAIN_1:9;
consider b being Object of such that
A4: f2 = id b by A2, Def19;
consider a being Object of such that
A5: f1 = id a by A1, Def19;
take [a,b] ; :: thesis: f = id [a,b]
thus f = id [a,b] by A3, A5, A4, CAT_2:41; :: thesis: verum