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 by ORDINAL1:def 12;
then A1 . m = {} by FUNCOP_1:7;
hence ( m <> n implies A1 . m misses A1 . n ) ; :: thesis: verum

end;

hence A1 is disjoint_valued ; :: thesis: verum