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 = <*p*> ^ (f |-- p)
let p be Element of D; :: thesis: for f being FinSequence of D st p in rng f holds
f :- p = <*p*> ^ (f |-- p)
let f be FinSequence of D; :: thesis: ( p in rng f implies f :- p = <*p*> ^ (f |-- p) )
assume p in rng f ; :: thesis: f :- p = <*p*> ^ (f |-- p)
hence <*p*> ^ (f |-- p) = <*p*> ^ (f /^ (p .. f)) by FINSEQ_5:35
.= f :- p by FINSEQ_5:def 2 ;
:: thesis: verum