let F be ManySortedSet of NAT ; :: thesis: for n being object holds
( n is Nat iff n in dom F )
let n be object ; :: thesis: ( n is Nat iff n in dom F )

hereby :: thesis: ( n in dom F implies n is Nat )

assume n is Nat ; :: thesis: n in dom F
then n in NAT by ORDINAL1:def 12;
hence n in dom F by PARTFUN1:def 2; :: thesis: verum

end;

assume n in dom F ; :: thesis: n is Nat
hence n is Nat ; :: thesis: verum