let x be set ; :: according to TARSKI:def 3,FINSEQ_1:def 4 :: thesis: ( not x in rng (idseq n) or x in REAL )
assume x in rng (idseq n) ; :: thesis: x in REAL
then consider y being set such that
A1: y in dom (idseq n) and
A2: x = (idseq n) . y by FUNCT_1:def 3;
A3: y in Seg n by A1, RELAT_1:45;
reconsider y = y as Element of NAT by A1;
(idseq n) . y = y by A3, FUNCT_1:18;
hence x in REAL by A2; :: thesis: verum