let n be Nat; :: thesis: for p being XFinSequence ex q being XFinSequence st p = (p | n) ^ q
let p be XFinSequence; :: thesis: ex q being XFinSequence st p = (p | n) ^ q

now :: thesis: ex q being XFinSequence st p = (p | n) ^ q

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

suppose n > len p ; :: thesis: ex q being XFinSequence st p = (p | n) ^ q

then Segm (len p) c= Segm n by NAT_1:39;
then A1: p | n = p by RELAT_1:68;
p ^ {} = p ;
hence ex q being XFinSequence st p = (p | n) ^ q by A1; :: thesis: verum

end;

suppose n <= len p ; :: thesis: ex q being XFinSequence st p = (p | n) ^ q

then reconsider n1 = (len p) - n as Element of NAT by NAT_1:21;
defpred S₁[ Nat] means for k being Nat st k = (len p) - $1 holds
ex q being XFinSequence st p = (p | k) ^ q;
A2: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A3: S₁[m] ; :: thesis: S₁[m + 1]
let k be Nat; :: thesis: ( k = (len p) - (m + 1) implies ex q being XFinSequence st p = (p | k) ^ q )
assume A4: k = (len p) - (m + 1) ; :: thesis: ex q being XFinSequence st p = (p | k) ^ q
consider q being XFinSequence such that
A5: p = (p | (k + 1)) ^ q by A3, A4;
Segm k c= Segm (k + 1) by NAT_1:39, NAT_1:11;
then A6: (p | (k + 1)) | k = p | k by RELAT_1:74;
(len p) - m <= (len p) - 0 by XREAL_1:10;
then len (p | (k + 1)) = k + 1 by Th51, A4;
then p | (k + 1) = ((p | (k + 1)) | k) ^ <%((p | (k + 1)) . k)%> by Th53;
then p = (p | k) ^ (<%((p | (k + 1)) . k)%> ^ q) by A5, A6, Th25;
hence ex q being XFinSequence st p = (p | k) ^ q ; :: thesis: verum

end;

( p | ((len p) - 0) = p & p ^ {} = p ) ;
then A7: S₁[ 0 ] ;
A8: for m being Nat holds S₁[m] from NAT_1:sch 2(A7, A2);
n = (len p) - n1 ;
hence ex q being XFinSequence st p = (p | n) ^ q by A8; :: thesis: verum

end;

end;

end;

hence ex q being XFinSequence st p = (p | n) ^ q ; :: thesis: verum