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

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