take rng (Ser (D, the Num of D)) ; :: thesis: ex N being Num of D st rng (Ser (D, the Num of D)) = rng (Ser (D,N))
thus ex N being Num of D st rng (Ser (D, the Num of D)) = rng (Ser (D,N)) ; :: thesis: verum