let k be natural Number ; :: thesis: for p being FinSequence st len p <= k holds
p * (idseq k) = p
let p be FinSequence; :: thesis: ( len p <= k implies p * (idseq k) = p )
assume A1: len p <= k ; :: thesis: p * (idseq k) = p
reconsider k = k as Element of NAT by ORDINAL1:def 12;
dom p = Seg (len p) by FINSEQ_1:def 3;
then dom p c= Seg k by A1, FINSEQ_1:5;
hence p * (idseq k) = p by RELAT_1:51; :: thesis: verum