let V, W be non empty set ; :: thesis: for f being FinSequence
for l being Function of V,W st rng f c= V holds
( l * f is W -valued & l * f is FinSequence-like )
let f be FinSequence; :: thesis: for l being Function of V,W st rng f c= V holds
( l * f is W -valued & l * f is FinSequence-like )
let l be Function of V,W; :: thesis: ( rng f c= V implies ( l * f is W -valued & l * f is FinSequence-like ) )
assume rng f c= V ; :: thesis: ( l * f is W -valued & l * f is FinSequence-like )
then rng f c= dom l by FUNCT_2:def 1;
hence ( l * f is W -valued & l * f is FinSequence-like ) by FINSEQ_1:16; :: thesis: verum