let z be set ; :: according to TARSKI:def 3,FINSEQ_1:def 4 :: thesis: ( not z in rng (i |-> x) or z in REAL )
assume z in rng (i |-> x) ; :: thesis: z in REAL
hence z in REAL ; :: thesis: verum