let p be FinSequence; :: thesis: for n being natural number holds
( p | (Seg n) = p iff len p <= n )
let n be natural number ; :: thesis: ( p | (Seg n) = p iff len p <= n )
n is Element of NAT by ORDINAL1:def 13;
hence ( p | (Seg n) = p implies len p <= n ) by TREES_1:1; :: 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:7;
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 set st x in dom p holds
p . x = p . x ;
hence p | (Seg n) = p by A1, FUNCT_1:68; :: thesis: verum