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