let D be non empty set ; :: thesis: for p being Element of D

for f being FinSequence of D holds 1 <= len (f :- p)

let p be Element of D; :: thesis: for f being FinSequence of D holds 1 <= len (f :- p)

let f be FinSequence of D; :: thesis: 1 <= len (f :- p)

len (f :- p) = len (<*p*> ^ (f /^ (p .. f))) by FINSEQ_5:def 2

.= (len <*p*>) + (len (f /^ (p .. f))) by FINSEQ_1:22

.= 1 + (len (f /^ (p .. f))) by FINSEQ_1:39 ;

hence 1 <= len (f :- p) by NAT_1:11; :: thesis: verum

for f being FinSequence of D holds 1 <= len (f :- p)

let p be Element of D; :: thesis: for f being FinSequence of D holds 1 <= len (f :- p)

let f be FinSequence of D; :: thesis: 1 <= len (f :- p)

len (f :- p) = len (<*p*> ^ (f /^ (p .. f))) by FINSEQ_5:def 2

.= (len <*p*>) + (len (f /^ (p .. f))) by FINSEQ_1:22

.= 1 + (len (f /^ (p .. f))) by FINSEQ_1:39 ;

hence 1 <= len (f :- p) by NAT_1:11; :: thesis: verum