let D be non empty set ; :: thesis: for f being FinSequence of D
for k being Element of NAT
for p being Element of D holds (<*p*> ^ f) | (k + 1) = <*p*> ^ (f | k)
let f be FinSequence of D; :: thesis: for k being Element of NAT
for p being Element of D holds (<*p*> ^ f) | (k + 1) = <*p*> ^ (f | k)
let k be Element of NAT ; :: thesis: for p being Element of D holds (<*p*> ^ f) | (k + 1) = <*p*> ^ (f | k)
let p be Element of D; :: thesis: (<*p*> ^ f) | (k + 1) = <*p*> ^ (f | k)
A1: f | (Seg k) = f | k by FINSEQ_1:def 15;
thus (<*p*> ^ f) | (k + 1) = (<*p*> ^ f) | (Seg (k + 1)) by FINSEQ_1:def 15
.= (<*p*> ^ f) | (Seg (k + (len <*p*>))) by FINSEQ_1:39
.= <*p*> ^ (f | k) by A1, Th16 ; :: thesis: verum