let p be FinSequence; :: thesis: for n being Nat holds
( p | (Seg n) = p iff len p <= n )
let n be Nat; :: thesis: ( p | (Seg n) = p iff len p <= n )
thus ( p | (Seg n) = p implies len p <= n ) by FINSEQ_1:86; :: thesis: ( len p <= n implies p | (Seg n) = p )
assume len p <= n ; :: thesis: p | (Seg n) = p
then Seg (len p) c= Seg n by FINSEQ_1:5;
then dom p c= Seg n by FINSEQ_1:def 3;
then A1: dom p = (dom p) /\ (Seg n) by XBOOLE_1:28;
for x being object st x in dom p holds
p . x = p . x ;
hence p | (Seg n) = p by A1, FUNCT_1:46; :: thesis: verum