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

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