let n be Nat; :: thesis: for D being non empty set
for p being Element of D
for f being FinSequence of D st len f <= n holds
Ins f,n,p = f ^ <*p*>
let D be non empty set ; :: thesis: for p being Element of D
for f being FinSequence of D st len f <= n holds
Ins f,n,p = f ^ <*p*>
let p be Element of D; :: thesis: for f being FinSequence of D st len f <= n holds
Ins f,n,p = f ^ <*p*>
let f be FinSequence of D; :: thesis: ( len f <= n implies Ins f,n,p = f ^ <*p*> )
assume A1: len f <= n ; :: thesis: Ins f,n,p = f ^ <*p*>
then f /^ n is empty by Th35;
hence Ins f,n,p = (f | n) ^ <*p*> by FINSEQ_1:47
.= f ^ <*p*> by A1, FINSEQ_1:79 ;
:: thesis: verum