take A1 = NAT --> ({} X); :: thesis: A1 is disjoint_valued
for m, n being Nat st m <> n holds
A1 . m misses A1 . n

proof

let m, n be Nat; :: thesis: ( m <> n implies A1 . m misses A1 . n )
( m in NAT & n in NAT ) by ORDINAL1:def 13;
then ( A1 . m = {} & A1 . n = {} ) by FUNCOP_1:13;
hence ( m <> n implies A1 . m misses A1 . n ) by XBOOLE_1:65; :: thesis: verum

end;

hence A1 is disjoint_valued by PROB_3:def 4; :: thesis: verum