let f be FinSequence; :: thesis: f /^ 0 = f
A1: 0 <= len f ;

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

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;
hence f /^ 0 = f by A2; :: thesis: verum