let D be non empty set ; :: thesis: for p being Element of D
for f being FinSequence of D holds (f :- p) :- p = f :- p
let p be Element of D; :: thesis: for f being FinSequence of D holds (f :- p) :- p = f :- p
let f be FinSequence of D; :: thesis: (f :- p) :- p = f :- p
A1: (<*p*> ^ (f /^ (p .. f))) /. 1 = p by FINSEQ_5:15;
thus (f :- p) :- p = (<*p*> ^ (f /^ (p .. f))) :- p by FINSEQ_5:def 2
.= <*p*> ^ (f /^ (p .. f)) by A1, Th44
.= f :- p by FINSEQ_5:def 2 ; :: thesis: verum