let t be FinSequence of INT ; :: thesis: t is FinSequence of REAL
now :: thesis: for i being Nat st i in dom t holds
t . i in REAL
let i be Nat; :: thesis: ( i in dom t implies t . i in REAL )
assume i in dom t ; :: thesis: t . i in REAL
then A1: t . i in rng t by FUNCT_1:def 3;
t . i in INT by A1;
hence t . i in REAL by NUMBERS:15; :: thesis: verum
end;
hence t is FinSequence of REAL by FINSEQ_2:12; :: thesis: verum