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:34
.= <*p*> ^ f by Th31 ; :: thesis: verum