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
then A1: p .. (f -: p) = p .. f by Th72;
thus (f -: p) -: p = (f -: p) | (p .. (f -: p)) by FINSEQ_5:def 1
.= (f | (p .. f)) | (p .. f) by A1, FINSEQ_5:def 1
.= f -: p by FINSEQ_5:def 1 ; :: thesis: verum