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