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

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