let f be FinSequence; :: thesis: for k being Nat
for p being set holds (<*p*> ^ f) | (k + 1) = <*p*> ^ (f | k)
let k be Nat; :: thesis: for p being set holds (<*p*> ^ f) | (k + 1) = <*p*> ^ (f | k)
let p be set ; :: thesis: (<*p*> ^ f) | (k + 1) = <*p*> ^ (f | k)
thus (<*p*> ^ f) | (k + 1) = (<*p*> ^ f) | (Seg (k + (len <*p*>))) by FINSEQ_1:39
.= <*p*> ^ (f | k) by Th14 ; :: thesis: verum