let D be set ; :: thesis: for p being FinSequence
for n being Element of NAT st p in D * holds
p | (Seg n) in D *
let p be FinSequence; :: thesis: for n being Element of NAT st p in D * holds
p | (Seg n) in D *
let n be Element of 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