let p be FinSequence; :: thesis: ( p /^ 0 = p & ( for i being Nat st i >= len p holds
p /^ i = {} ) )
A1: 0 <= len p by NAT_1:2;

A2: now :: thesis: for i being Nat st 1 <= i & i <= len (p /^ 0) holds
(p /^ 0) . i = p . i

let i be Nat; :: thesis: ( 1 <= i & i <= len (p /^ 0) implies (p /^ 0) . i = p . i )
assume ( 1 <= i & i <= len (p /^ 0) ) ; :: thesis: (p /^ 0) . i = p . i
then i in dom (p /^ 0) by FINSEQ_3:25;
hence (p /^ 0) . i = p . (i + 0) by A1, RFINSEQ:def 1
.= p . i ;
:: thesis: verum

end;

len (p /^ 0) = (len p) - 0 by A1, RFINSEQ:def 1
.= len p ;
hence p /^ 0 = p by A2; :: thesis: for i being Nat st i >= len p holds
p /^ i = {}
let i be Nat; :: thesis: ( i >= len p implies p /^ i = {} )
assume i >= len p ; :: thesis: p /^ i = {}
then ( ( i = len p & len (p /^ (len p)) = (len p) - (len p) ) or i > len p ) by XXREAL_0:1, RFINSEQ:def 1;
hence p /^ i = {} by RFINSEQ:def 1; :: thesis: verum