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

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

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

A2: 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;

len (f /^ 0 ) = (len f) - 0 by A1, Th16
.= len f ;
hence f /^ 0 = f by A2, AFINSQ_1:11; :: thesis: verum

end;

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

then f /^ 0 = {} by Th15;
hence f /^ 0 = f by A3; :: thesis: verum

end;

end;