let f be XFinSequence; :: thesis: f /^ 0 = f

per cases ( 0 < len f or 0 >= len f ) ;

suppose 0 < len f ; :: thesis: f /^ 0 = f

then A2: len (f /^ 0 ) = (len f) - 0 by TH80b
.= len f ;

now

let i be Element of NAT ; :: thesis: ( i < len (f /^ 0 ) implies (f /^ 0 ) . i = f . i )
assume i < len (f /^ 0 ) ; :: thesis: (f /^ 0 ) . i = f . i
then i in dom (f /^ 0 ) by NAT_1:45;
hence (f /^ 0 ) . i = f . (i + 0 ) by Def2
.= f . i ;
:: thesis: verum

end;

hence f /^ 0 = f by A2, AFINSQ_1:11; :: thesis: verum

end;

suppose B0: 0 >= len f ; :: thesis: f /^ 0 = f

then f /^ 0 = {} by TH80e;
hence f /^ 0 = f by B0; :: thesis: verum

end;

end;