let f be FinSequence of NAT ; :: thesis: f is FinSequence of REAL

for n being Nat st n in dom f holds

f . n in REAL by XREAL_0:def 1;

hence f is FinSequence of REAL by FINSEQ_2:12; :: thesis: verum

for n being Nat st n in dom f holds

f . n in REAL by XREAL_0:def 1;

hence f is FinSequence of REAL by FINSEQ_2:12; :: thesis: verum