let f be Function; :: thesis: for p being XFinSequence st rng p c= dom f holds
f * p is XFinSequence
let p be XFinSequence; :: thesis: ( rng p c= dom f implies f * p is XFinSequence )
assume rng p c= dom f ; :: thesis: f * p is XFinSequence
then dom (f * p) = len p by RELAT_1:27;
hence f * p is XFinSequence by ORDINAL1:def 7; :: thesis: verum