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