let n be Element of NAT ; :: thesis: for f being FinSequence st len f = 0 holds
f /^ n = f
let f be FinSequence; :: thesis: ( len f = 0 implies f /^ n = f )
assume A1: len f = 0 ; :: thesis: f /^ n = f

per cases ( n = 0 or n > 0 ) ;

suppose A2: n = 0 ; :: thesis: f /^ n = f

then len (f /^ n) = (len f) - n by RFINSEQ:def 1
.= 0 by A1, A2 ;
then f /^ n = {} ;
hence f /^ n = f by A1; :: thesis: verum

end;

suppose n > 0 ; :: thesis: f /^ n = f

then f /^ n = {} by A1, RFINSEQ:def 1;
hence f /^ n = f by A1; :: thesis: verum

end;

end;