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

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

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

A2: now

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

end;

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

end;

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

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

end;

end;