set NS = { i where i is Nat : ( i in dom f & 1 <= i & i <= n & f . i <> - 1 ) } ;

{ i where i is Nat : ( i in dom f & 1 <= i & i <= n & f . i <> - 1 ) } c= NAT

{ i where i is Nat : ( i in dom f & 1 <= i & i <= n & f . i <> - 1 ) } c= NAT

proof

hence
{ i where i is Nat : ( i in dom f & 1 <= i & i <= n & f . i <> - 1 ) } is Subset of NAT
; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { i where i is Nat : ( i in dom f & 1 <= i & i <= n & f . i <> - 1 ) } or x in NAT )

assume x in { i where i is Nat : ( i in dom f & 1 <= i & i <= n & f . i <> - 1 ) } ; :: thesis: x in NAT

then ex k being Nat st

( x = k & k in dom f & 1 <= k & k <= n & f . k <> - 1 ) ;

hence x in NAT ; :: thesis: verum

end;assume x in { i where i is Nat : ( i in dom f & 1 <= i & i <= n & f . i <> - 1 ) } ; :: thesis: x in NAT

then ex k being Nat st

( x = k & k in dom f & 1 <= k & k <= n & f . k <> - 1 ) ;

hence x in NAT ; :: thesis: verum