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

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