let D be non empty set ; :: thesis: for p being Element of D
for f being FinSequence of D st p in rng f holds
f -: p = (f -| p) ^ <*p*>
let p be Element of D; :: thesis: for f being FinSequence of D st p in rng f holds
f -: p = (f -| p) ^ <*p*>
let f be FinSequence of D; :: thesis: ( p in rng f implies f -: p = (f -| p) ^ <*p*> )
assume p in rng f ; :: thesis: f -: p = (f -| p) ^ <*p*>
hence (f -| p) ^ <*p*> = f | (p .. f) by FINSEQ_5:24
.= f -: p by FINSEQ_5:def 1 ;
:: thesis: verum