let f be Function; :: thesis: for p being FinSequence st rng p c= dom f holds
f * p is FinSequence
let p be FinSequence; :: thesis: ( rng p c= dom f implies f * p is FinSequence )
assume rng p c= dom f ; :: thesis: f * p is FinSequence
then dom (f * p) = dom p by RELAT_1:27
.= Seg (len p) by Def3 ;
hence f * p is FinSequence by Def2; :: thesis: verum