let D be set ; :: thesis: for p being FinSequence
for n being Nat st p in D * holds
p | (Seg n) in D *
let p be FinSequence; :: thesis: for n being Nat st p in D * holds
p | (Seg n) in D *
let n be Nat; :: thesis: ( p in D * implies p | (Seg n) in D * )
assume p in D * ; :: thesis: p | (Seg n) in D *
then p is FinSequence of D by FINSEQ_1:def 11;
then p | (Seg n) is FinSequence of D by FINSEQ_1:18;
hence p | (Seg n) in D * by FINSEQ_1:def 11; :: thesis: verum