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: len (f /^ 0 ) = (len f) - 0 by RFINSEQ:def 2
.= len f ;

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:27;
hence (f /^ 0 ) . i = f . (i + 0 ) by A1, RFINSEQ:def 2
.= f . i ;
:: thesis: verum

end;

hence f /^ 0 = f by A2, FINSEQ_1:18; :: thesis: verum