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

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