let f be FinSequence of NAT ; :: thesis: f is FinSequence of REAL
for n being natural number st n in dom f holds
f . n in REAL ;
hence f is FinSequence of REAL by FINSEQ_2:12; :: thesis: verum