let D be set ; :: thesis: for f being FinSequence of D holds f /^ 0 = f
let f be FinSequence of D; :: thesis: f /^ 0 = f
A1: 0 <= len f ;

A2: now

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

end;

len (f /^ 0) = (len f) - 0 by RFINSEQ:def 1
.= len f ;
hence f /^ 0 = f by A2, FINSEQ_1:14; :: thesis: verum