let V, W be non empty set ; :: thesis: for A being finite Subset of V

for l being Function of V,W holds

( l * (canFS A) is W -valued & l * (canFS A) is FinSequence-like )

let A be finite Subset of V; :: thesis: for l being Function of V,W holds

( l * (canFS A) is W -valued & l * (canFS A) is FinSequence-like )

let l be Function of V,W; :: thesis: ( l * (canFS A) is W -valued & l * (canFS A) is FinSequence-like )

set p = l * (canFS A);

set f = canFS A;

dom l = V by FUNCT_2:def 1;

then rng (canFS A) c= dom l by XBOOLE_1:1;

hence ( l * (canFS A) is W -valued & l * (canFS A) is FinSequence-like ) by FINSEQ_1:16; :: thesis: verum

for l being Function of V,W holds

( l * (canFS A) is W -valued & l * (canFS A) is FinSequence-like )

let A be finite Subset of V; :: thesis: for l being Function of V,W holds

( l * (canFS A) is W -valued & l * (canFS A) is FinSequence-like )

let l be Function of V,W; :: thesis: ( l * (canFS A) is W -valued & l * (canFS A) is FinSequence-like )

set p = l * (canFS A);

set f = canFS A;

dom l = V by FUNCT_2:def 1;

then rng (canFS A) c= dom l by XBOOLE_1:1;

hence ( l * (canFS A) is W -valued & l * (canFS A) is FinSequence-like ) by FINSEQ_1:16; :: thesis: verum