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 X: f * (canFS (dom f)) is FinSequence by FINSEQ_1:20;
rng (f * (canFS (dom f))) c= REAL ;
hence f * (canFS (dom f)) is FinSequence of REAL by FINSEQ_1:def 4, X; :: thesis: verum