let k be Element of NAT ; :: thesis: for D being set
for p being XFinSequence of D holds p | k is XFinSequence of D
let D be set ; :: thesis: for p being XFinSequence of D holds p | k is XFinSequence of D
let p be XFinSequence of D; :: thesis: p | k is XFinSequence of D
( rng (p | k) c= rng p & rng p c= D ) by ORDINAL1:def 8;
then rng (p | k) c= D by XBOOLE_1:1;
hence p | k is XFinSequence of D by Th12, ORDINAL1:def 8; :: thesis: verum