set i = the Element of N;
reconsider A = rng the mapping of (N | the Element of N) as Subset of S ;
take A ; :: thesis: ex i being Element of N st A = rng the mapping of (N | i)
take the Element of N ; :: thesis: A = rng the mapping of (N | the Element of N)
thus A = rng the mapping of (N | the Element of N) ; :: thesis: verum