let Omega be non empty finite set ; :: thesis: for f being PartFunc of Omega,REAL holds f * (canFS (dom f)) is FinSequence of REAL
let f be PartFunc of Omega,REAL; :: thesis: f * (canFS (dom f)) is FinSequence of REAL
rng (canFS (dom f)) c= dom f ;
then A1: f * (canFS (dom f)) is FinSequence by FINSEQ_1:16;
rng (f * (canFS (dom f))) c= REAL ;
hence f * (canFS (dom f)) is FinSequence of REAL by A1, FINSEQ_1:def 4; :: thesis: verum