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 )

then n in NAT by PARTFUN1:def 2;

hence n is Nat ; :: thesis: verum

( 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 in dom F
; :: thesis: n is Natassume
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;then n in NAT by ORDINAL1:def 12;

hence n in dom F by PARTFUN1:def 2; :: thesis: verum

then n in NAT by PARTFUN1:def 2;

hence n is Nat ; :: thesis: verum