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