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 :: thesis: for i being Nat st i < len (p /^ 0) holds
(p /^ 0) . i = p . i

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
hence (p /^ 0) . i = p . (i + 0) by Def2, AFINSQ_1:86
.= p . i ;
:: thesis: verum

end;

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

end;

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

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

end;

end;