let D be non empty set ; :: thesis: for p being Element of D
for f being FinSequence of D holds Ins f,0 ,p = <*p*> ^ f
let p be Element of D; :: thesis: for f being FinSequence of D holds Ins f,0 ,p = <*p*> ^ f
let f be FinSequence of D; :: thesis: Ins f,0 ,p = <*p*> ^ f
thus Ins f,0 ,p = <*p*> ^ (f /^ 0 ) by FINSEQ_1:47
.= <*p*> ^ f by Th31 ; :: thesis: verum