consider N being Num of D;
set S = Ser (D,N);
reconsider SER = rng (Ser (D,N)) as non empty Subset of ExtREAL ;
take SER ; :: thesis: ex N being Num of D st SER = rng (Ser (D,N))
thus ex N being Num of D st SER = rng (Ser (D,N)) ; :: thesis: verum