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

proof

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;

hence { i where i is Nat : ( i in dom f & 1 <= i & i <= n & f . i <> - 1 ) } is Subset of NAT ; :: thesis: verum